1  /-
  2  Copyright (c) 2017 Microsoft Corporation. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Mario Carneiro
  5  
  6  Coinductive formalization of unbounded computations.
  7  -/
  8  import data.stream logic.relator tactic.basic
src         └─────────┘ └───────────┘ └──────────┘
  9  universes u v w
 10  
 11  /-
 12  coinductive computation (α : Type u) : Type u
 13  | return : α → computation α
 14  | think : computation α → computation α
 15  -/
 16  
 17  /-- `computation α` is the type of unbounded computations returning `α`.
 18    An element of `computation α` is an infinite sequence of `option α` such
 19    that if `f n = some a` for some `n` then it is constantly `some a` after that. -/
 20  def computation (α : Type u) : Type u :=
 21  { f : stream (option α) // ∀ {n a}, f n = some a → f (n+1) = some a }
id        └────┘  └────┘                └──┘          └──┘ 
src       └────┘  └────┘                     └──┘             └──┘
typ       └────┘  └────┘                └──┘          └──┘ 
 22  
 23  namespace computation
 24  variables {α : Type u} {β : Type v} {γ : Type w}
id             
typ            
 25  
 26  -- constructors
 27  /-- `return a` is the computation that immediately terminates with result `a`. -/
 28  def return (a : α) : computation α := ⟨stream.const (some a), λn a', id⟩
id                       └─────────┘      └──────────┘  └──┘      └┘  └┘
src                       └─────────┘       └──────────┘  └──┘            └┘
typ                      └─────────┘      └──────────┘  └──┘      └┘  └┘
doc                       └─────────┘
 29  
 30  instance : has_coe_t α (computation α) := ⟨return⟩ -- note [use has_coe_t]
id              └───────┘   └─────────┘       └────┘
src             └───────┘    └─────────┘        └────┘
typ             └───────┘   └─────────┘       └────┘
doc             └───────┘    └─────────┘        └────┘
 31  
 32  /-- `think c` is the computation that delays for one "tick" and then performs
 33    computation `c`. -/
 34  def think (c : computation α) : computation α :=
id                  └─────────┘     └─────────┘ 
src                 └─────────┘      └─────────┘
typ                 └─────────┘     └─────────┘ 
doc                 └─────────┘      └─────────┘
 35  ⟨none :: c.1, λn a h, by {cases n with n, contradiction, exact c.2 h}⟩
id    └──┘ └┘                                                    
src   └──┘ └┘                 └────┘ └─────┘  └───────────┘  └────┘ └─┘
typ   └──┘ └┘             └────┘└─────┘  └───────────┘  └────┘└─┘
doc                            └────┘ └─────┘  └───────────┘  └────┘ └─┘
txt                            └────┘ └─────┘  └───────────┘  └────┘ └─┘
par                            └────┘ └─────┘  └───────────┘  └────┘ └─┘
pid                                  └─────┘                       └─┘
st                           └──────────────┘└─────────────┘└───────────┘└┘
 36  
 37  /-- `thinkN c n` is the computation that delays for `n` ticks and then performs
 38    computation `c`. -/
 39  def thinkN (c : computation α) : ℕ → computation α
id                   └─────────┘       └─────────┘ 
src                  └─────────┘         └─────────┘
typ                  └─────────┘       └─────────┘ 
doc                  └─────────┘          └─────────┘
 40  | 0 := c
id          
typ         
 41  | (n+1) := think (thinkN n)
id            └───┘  └────┘
src            └───┘
typ           └───┘  └────┘
doc             └───┘
 42  
 43  -- check for immediate result
 44  /-- `head c` is the first step of computation, either `some a` if `c = return a`
 45    or `none` if `c = think c'`. -/
 46  def head (c : computation α) : option α := c.1.head
id                 └─────────┘     └────┘      └──┘
src                └─────────┘      └────┘        └──┘
typ                └─────────┘     └────┘      └──┘
doc                └─────────┘
 47  
 48  -- one step of computation
 49  /-- `tail c` is the remainder of computation, either `c` if `c = return a`
 50    or `c'` if `c = think c'`. -/
 51  def tail (c : computation α) : computation α :=
id                 └─────────┘     └─────────┘ 
src                └─────────┘      └─────────┘
typ                └─────────┘     └─────────┘ 
doc                └─────────┘      └─────────┘
 52  ⟨c.1.tail, λ n a, let t := c.2 in t⟩
id     └──┘                     
src     └──┘                    
typ    └──┘                     
 53  
 54  /-- `empty α` is the computation that never returns, an infinite sequence of
 55    `think`s. -/
 56  def empty (α) : computation α := ⟨stream.const none, λn a', id⟩
id                   └─────────┘      └──────────┘ └──┘    └┘  └┘
src                  └─────────┘       └──────────┘ └──┘         └┘
typ                  └─────────┘      └──────────┘ └──┘    └┘  └┘
doc                  └─────────┘
 57  
 58  instance : inhabited (computation α) := ⟨empty _⟩
id              └───────┘  └─────────┘       └───┘
src             └───────┘  └─────────┘        └───┘
typ             └───────┘  └─────────┘       └───┘
doc                        └─────────┘        └───┘
 59  
 60  /-- `run_for c n` evaluates `c` for `n` steps and returns the result, or `none`
 61    if it did not terminate after `n` steps. -/
 62  def run_for : computation α → ℕ → option α := subtype.val
id                 └─────────┘       └────┘     └─────────┘
src                └─────────┘        └────┘      └─────────┘
typ                └─────────┘       └────┘     └─────────┘
doc                └─────────┘
 63  
 64  /-- `destruct c` is the destructor for `computation α` as a coinductive type.
 65    It returns `inl a` if `c = return a` and `inr c'` if `c = think c'`. -/
 66  def destruct (c : computation α) : α ⊕ computation α :=
id                     └─────────┘       └─────────┘ 
src                    └─────────┘         └─────────┘
typ                    └─────────┘       └─────────┘ 
doc                    └─────────┘          └─────────┘
 67  match c.1 0 with
id         
src         
typ        
 68  | none := sum.inr (tail c)
id     └──┘    └─────┘  └──┘ 
src    └──┘    └─────┘  └──┘
typ    └──┘    └─────┘  └──┘ 
doc                     └──┘
 69  | some a := sum.inl a
id     └──┘     └─────┘
src    └──┘      └─────┘
typ    └──┘     └─────┘
 70  end
 71  
 72  /-- `run c` is an unsound meta function that runs `c` to completion, possibly
 73    resulting in an infinite loop in the VM. -/
 74  meta def run : computation α → α | c :=
id                  └─────────┘      
src                 └─────────┘
typ                 └─────────┘      
doc                 └─────────┘
 75  match destruct c with
id         └──────┘
src        └──────┘
typ        └──────┘
doc        └──────┘
 76  | sum.inl a := a
id     └─────┘ 
src    └─────┘
typ    └─────┘ 
 77  | sum.inr ca := run ca
id     └─────┘ └┘    └─┘
src    └─────┘
typ    └─────┘ └┘    └─┘
 78  end
 79  
 80  theorem destruct_eq_ret {s : computation α} {a : α} :
id                                └─────────┘        
src                               └─────────┘
typ                               └─────────┘        
doc                               └─────────┘
 81    destruct s = sum.inl a → s = return a :=
id     └──────┘   └─────┘      └────┘ 
src    └──────┘    └─────┘        └────┘
typ    └──────┘   └─────┘      └────┘ 
doc    └──────┘                     └────┘
 82  begin
st   └─────
 83    dsimp [destruct],
id            └──────┘
src    └─────┘└──────┘
typ    └─────┘└──────┘
doc    └─────┘└──────┘
txt    └─────┘        
par    └─────┘        
pid                 
st   ─────────────────┘└─
 84    induction f0 : s.1 0; intro h,
id                    
src    └────────┘  └─┘ └──┘  └─────┘
typ    └────────┘  └─┘└──┘  └─────┘
doc    └────────┘  └─┘ └──┘  └─────┘
txt    └────────┘  └─┘ └──┘  └─────┘
par    └────────┘  └─┘ └──┘  └─────┘
pid               └─┘ └─┘       └┘
st   ──────────────────────────────┘└─
 85    { contradiction },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ───┘└────────────┘└┘
 86    { apply subtype.eq, funext n,
id             └────────┘
src      └────┘└────────┘  └──────┘
typ      └────┘└────────┘  └──────┘
doc      └────┘            └──────┘
txt      └────┘            └──────┘
par      └────┘            └──────┘
pid                             └┘
st   ───────────────────┘└────────┘└─
 87      induction n with n IH,
id                 
src      └────────┘ └────────┘
typ      └────────┘└────────┘
doc      └────────┘ └────────┘
txt      └────────┘ └────────┘
par      └────────┘ └────────┘
pid                └───────┘
st   ────────────────────────┘└─
 88      { injection h with h', rwa h' at f0 },
id                                 └┘
src        └────────┘ └──────┘  └──┘  └─────┘
typ        └────────┘└──────┘  └──┘└┘└─────┘
doc        └────────┘ └──────┘  └──┘  └─────┘
txt        └────────┘ └──────┘  └──┘  └─────┘
par        └────────┘ └──────┘  └──┘  └─────┘
pid                  └──────┘       └────┘
st   ─────┘└─────────────────┘└─────────────┘└┘
 89      { exact s.2 IH } }
id                  └┘
src        └────┘ └─┘  
typ        └────┘└─┘└┘
doc        └────┘ └─┘  
txt        └────┘ └─┘  
par        └────┘ └─┘  
pid              └─┘  
st   ──────────────────┘└───
 90  end
st   ──┘
 91  
 92  theorem destruct_eq_think {s : computation α} {s'} :
id                                  └─────────┘ 
src                                 └─────────┘
typ                                 └─────────┘ 
doc                                 └─────────┘
 93    destruct s = sum.inr s' → s = think s' :=
id     └──────┘   └─────┘ └┘     └───┘ └┘
src    └──────┘    └─────┘         └───┘
typ    └──────┘   └─────┘ └┘     └───┘ └┘
doc    └──────┘                      └───┘
 94  begin
st   └─────
 95    dsimp [destruct],
id            └──────┘
src    └─────┘└──────┘
typ    └─────┘└──────┘
doc    └─────┘└──────┘
txt    └─────┘        
par    └─────┘        
pid                 
st   ─────────────────┘└─
 96    induction f0 : s.1 0 with a'; intro h,
id                    
src    └────────┘  └─┘ └──────────┘  └─────┘
typ    └────────┘  └─┘└──────────┘  └─────┘
doc    └────────┘  └─┘ └──────────┘  └─────┘
txt    └────────┘  └─┘ └──────────┘  └─────┘
par    └────────┘  └─┘ └──────────┘  └─────┘
pid               └─┘ └─┘└┘└─────┘       └┘
st   ──────────────────────────────────────┘└─
 97    { injection h with h', rw ←h',
id                               └┘
src      └────────┘ └──────┘  └──┘
typ      └────────┘└──────┘  └──┘└┘
doc      └────────┘ └──────┘  └──┘
txt      └────────┘ └──────┘  └──┘
par      └────────┘ └──────┘  └──┘
pid                └──────┘    └┘
st   ───┘└─────────────────┘└──────┘└─
 98      cases s with f al,
id             
src      └────┘ └────────┘
typ      └────┘└────────┘
doc      └────┘ └────────┘
txt      └────┘ └────────┘
par      └────┘ └────────┘
pid            └────────┘
st   ────────────────────┘└─
 99      apply subtype.eq, dsimp [think, tail],
id             └────────┘         └───┘  └──┘
src      └────┘└────────┘  └─────┘└───┘└┘└──┘
typ      └────┘└────────┘  └─────┘└───┘└┘└──┘
doc      └────┘            └─────┘└───┘└┘└──┘
txt      └────┘            └─────┘     └┘    
par      └────┘            └─────┘     └┘    
pid                                 └┘    
st   ───────────────────┘└───────────────────┘└─
100      rw ←f0, exact (stream.eta f).symm },
id           └┘         └────────┘ 
src      └──┘    └────┘ └────────┘ └─────┘
typ      └──┘└┘  └────┘ └────────┘└─────┘
doc      └──┘    └────┘            └─────┘
txt      └──┘    └────┘            └─────┘
par      └──┘    └────┘            └─────┘
pid        └┘                     └───┘└┘
st   ─────────┘└──────────────────────────┘└┘
101    { contradiction }
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid                   
st   ─────────────────┘└─
102  end
st   ──┘
103  
104  @[simp] theorem destruct_ret (a : α) : destruct (return a) = sum.inl a := rfl
id                                         └──────┘  └────┘    └─────┘     └─┘
src                                         └──────┘  └────┘     └─────┘      └─┘
typ                                        └──────┘  └────┘    └─────┘     └─┘
doc    └──┘                                 └──────┘  └────┘
105  
106  @[simp] theorem destruct_think : ∀ s : computation α, destruct (think s) = sum.inr s
id                                         └─────────┘   └──────┘  └───┘    └─────┘ 
src                                         └─────────┘    └──────┘  └───┘     └─────┘
typ                                        └─────────┘   └──────┘  └───┘    └─────┘ 
doc    └──┘                                 └─────────┘    └──────┘  └───┘
107  | ⟨f, al⟩ := rfl
id                └─┘
src               └─┘
typ               └─┘
108  
109  @[simp] theorem destruct_empty : destruct (empty α) = sum.inr (empty α) := rfl
id                                    └──────┘  └───┘    └─────┘  └───┘      └─┘
src                                   └──────┘  └───┘     └─────┘  └───┘       └─┘
typ                                   └──────┘  └───┘    └─────┘  └───┘      └─┘
doc    └──┘                           └──────┘  └───┘               └───┘
110  
111  @[simp] theorem head_ret (a : α) : head (return a) = some a := rfl
id                                     └──┘  └────┘    └──┘     └─┘
src                                     └──┘  └────┘     └──┘      └─┘
typ                                    └──┘  └────┘    └──┘     └─┘
doc    └──┘                             └──┘  └────┘
112  
113  @[simp] theorem head_think (s : computation α) : head (think s) = none := rfl
id                                   └─────────┘     └──┘  └───┘    └──┘    └─┘
src                                  └─────────┘      └──┘  └───┘     └──┘    └─┘
typ                                  └─────────┘     └──┘  └───┘    └──┘    └─┘
doc    └──┘                          └─────────┘      └──┘  └───┘
114  
115  @[simp] theorem head_empty : head (empty α) = none := rfl
id                                └──┘  └───┘    └──┘    └─┘
src                               └──┘  └───┘     └──┘    └─┘
typ                               └──┘  └───┘    └──┘    └─┘
doc    └──┘                       └──┘  └───┘
116  
117  @[simp] theorem tail_ret (a : α) : tail (return a) = return a := rfl
id                                     └──┘  └────┘    └────┘     └─┘
src                                     └──┘  └────┘     └────┘      └─┘
typ                                    └──┘  └────┘    └────┘     └─┘
doc    └──┘                             └──┘  └────┘      └────┘
118  
119  @[simp] theorem tail_think (s : computation α) : tail (think s) = s :=
id                                   └─────────┘     └──┘  └───┘    
src                                  └─────────┘      └──┘  └───┘    
typ                                  └─────────┘     └──┘  └───┘    
doc    └──┘                          └─────────┘      └──┘  └───┘
120  by cases s with f al; apply subtype.eq; dsimp [tail, think]; rw [stream.tail_cons]
id                              └────────┘         └──┘  └───┘       └──────────────┘
src     └────┘ └────────┘  └────┘└────────┘  └─────┘└──┘└┘└───┘  └──┘└──────────────┘└─
typ     └────┘└────────┘  └────┘└────────┘  └─────┘└──┘└┘└───┘  └──┘└──────────────┘└─
doc     └────┘ └────────┘  └────┘            └─────┘└──┘└┘└───┘  └──┘                └─
txt     └────┘ └────────┘  └────┘            └─────┘    └┘       └──┘                └─
par     └────┘ └────────┘  └────┘            └─────┘    └┘       └──┘                └─
pid           └────────┘                            └┘         └┘                
st     └─────────────────────────────────────────────────────────────┘└──────────────┘
121  
src  
typ  
doc  
txt  
par  
pid  
st   
122  @[simp] theorem tail_empty : tail (empty α) = empty α := rfl
id                                └──┘  └───┘    └───┘     └─┘
src                               └──┘  └───┘     └───┘      └─┘
typ                               └──┘  └───┘    └───┘     └─┘
doc    └──┘                       └──┘  └───┘      └───┘
123  
124  theorem think_empty : empty α = think (empty α) :=
id                         └───┘   └───┘  └───┘ 
src                        └───┘    └───┘  └───┘
typ                        └───┘   └───┘  └───┘ 
doc                        └───┘     └───┘  └───┘
125  destruct_eq_think destruct_empty
id   └───────────────┘ └────────────┘
src  └───────────────┘ └────────────┘
typ  └───────────────┘ └────────────┘
126  
127  def cases_on {C : computation α → Sort v} (s : computation α)
id                     └─────────┘                 └─────────┘ 
src                    └─────────┘                  └─────────┘
typ                    └─────────┘                 └─────────┘ 
doc                    └─────────┘                  └─────────┘
128    (h1 : ∀ a, C (return a)) (h2 : ∀ s, C (think s)) : C s := begin
id                 └────┘                └───┘       
src                  └────┘                   └───┘
typ                └────┘                └───┘       
doc                  └────┘                   └───┘
st                                                               └─────
129    induction H : destruct s with v v,
id                   └──────┘ 
src    └────────┘ └─┘└──────┘ └───────┘
typ    └────────┘ └─┘└──────┘└───────┘
doc    └────────┘ └─┘└──────┘ └───────┘
txt    └────────┘ └─┘         └───────┘
par    └────────┘ └─┘         └───────┘
pid              └─┘         └──────┘
st   ──────────────────────────────────┘└─
130    { rw destruct_eq_ret H, apply h1 },
id          └─────────────┘ 
src      └─┘└─────────────┘   └────┘  
typ      └─┘└─────────────┘  └────┘  
doc      └─┘                  └────┘  
txt      └─┘                  └────┘  
par      └─┘                  └────┘  
pid                                 
st   ───┘└──────────────────┘└─────────┘└┘
131    { cases v with a s', rw destruct_eq_think H, apply h2 }
id                            └───────────────┘ 
src      └────┘ └────────┘  └─┘└───────────────┘   └────┘  
typ      └────┘└────────┘  └─┘└───────────────┘  └────┘  
doc      └────┘ └────────┘  └─┘                    └────┘  
txt      └────┘ └────────┘  └─┘                    └────┘  
par      └────┘ └────────┘  └─┘                    └────┘  
pid            └────────┘                               
st   ────────────────────┘└──────────────────────┘└─────────┘└─
132  end
st   ──┘
133  
134  def corec.F (f : β → α ⊕ β) : α ⊕ β → option α × (α ⊕ β)
id                                 └────┘      
src                                      └────┘       
typ                                └────┘      
135  | (sum.inl a) := (some a, sum.inl a)
id      └─────┘      └──┘    └─────┘
src     └─────┘       └──┘    └─────┘
typ     └─────┘      └──┘    └─────┘
136  | (sum.inr b) := (match f b with
id      └─────┘            
src     └─────┘       
typ     └─────┘            
137    | sum.inl a := some a
id       └─────┘     └──┘
src      └─────┘      └──┘
typ      └─────┘     └──┘
138    | sum.inr b' := none
id       └─────┘       └──┘
src      └─────┘       └──┘
typ      └─────┘       └──┘
139    end, f b)
id          
typ         
140  
141  /-- `corec f b` is the corecursor for `computation α` as a coinductive type.
142    If `f b = inl a` then `corec f b = return a`, and if `f b = inl b'` then
143    `corec f b = think (corec f b')`. -/
144  def corec (f : β → α ⊕ β) (b : β) : computation α :=
id                                  └─────────┘ 
src                                     └─────────┘
typ                                 └─────────┘ 
doc                                      └─────────┘
145  begin
st   └─────
146    refine ⟨stream.corec' (corec.F f) (sum.inr b), λn a' h, _⟩,
id             └───────────┘  └─────┘    └─────┘ 
src    └─────┘ └───────────┘ └─────┘ └┘ └─────┘ └─┘ └────────┘
typ    └─────┘ └───────────┘ └─────┘└┘ └─────┘└─┘ └────────┘
doc    └─────┘                       └┘         └─┘ └────────┘
txt    └─────┘                       └┘         └─┘ └────────┘
par    └─────┘                       └┘         └─┘ └────────┘
pid                                 └┘         └─┘ └────────┘
st   ───────────────────────────────────────────────────────────┘└─
147    rw stream.corec'_eq,
id        └──────────────┘
src    └─┘└──────────────┘
typ    └─┘└──────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────┘└─
148    change stream.corec' (corec.F f) (corec.F f (sum.inr b)).2 n = some a',
id            └───────────┘              └─────┘   └─────┘        └──┘ └┘
src    └─────┘└───────────┘         └┘ └─────┘  └─────┘ └───┘ └──┘
typ    └─────┘└───────────┘         └┘ └─────┘ └─────┘└───┘└──┘└┘
doc    └─────┘                      └┘                  └───┘      
txt    └─────┘                      └┘                  └───┘      
par    └─────┘                      └┘                  └───┘      
pid                                └┘                  └───┘      
st   ───────────────────────────────────────────────────────────────────────┘└─
149    revert h, generalize : sum.inr b = o, revert o,
id                            └─────┘ 
src    └──────┘  └───────────┘└─────┘     └──────┘
typ    └──────┘  └───────────┘└─────┘    └──────┘
doc    └──────┘  └───────────┘            └──────┘
txt    └──────┘  └───────────┘            └──────┘
par    └──────┘  └───────────┘            └──────┘
pid          └┘                              └┘
st   ─────────┘└──────────────────────────┘└────────┘└─
150    induction n with n IH; intro o,
id               
src    └────────┘ └────────┘  └─────┘
typ    └────────┘└────────┘  └─────┘
doc    └────────┘ └────────┘  └─────┘
txt    └────────┘ └────────┘  └─────┘
par    └────────┘ └────────┘  └─────┘
pid              └───────┘       └┘
st   ───────────────────────────────┘└─
151    { change (corec.F f o).1 = some a' → (corec.F f (corec.F f o).2).1 = some a',
id                                                     └─────┘           └──┘ └┘
src      └─────┘          └──┘                  └─────┘  └─────┘ └──┘
typ      └─────┘          └──┘                 └─────┘└─────┘ └──┘└┘
doc      └─────┘          └──┘                           └─────┘     
txt      └─────┘          └──┘                           └─────┘     
par      └─────┘          └──┘                           └─────┘     
pid                      └──┘                           └─────┘     
st   ───┘└────────────────────────────────────────────────────────────────────────┘└─
152      cases o with a b; intro h, { exact h },
id                                         
src      └────┘ └───────┘  └─────┘    └────┘ 
typ      └────┘└───────┘  └─────┘    └────┘
doc      └────┘ └───────┘  └─────┘    └────┘ 
txt      └────┘ └───────┘  └─────┘    └────┘ 
par      └────┘ └───────┘  └─────┘    └────┘ 
pid            └───────┘       └┘          
st   ────────────────────────────┘└──┘└──────┘└┘
153      dsimp [corec.F] at h, dsimp [corec.F],
id              └─────┘               └─────┘
src      └─────┘└─────┘└────┘  └─────┘└─────┘
typ      └─────┘└─────┘└────┘  └─────┘└─────┘
doc      └─────┘       └────┘  └─────┘       
txt      └─────┘       └────┘  └─────┘       
par      └─────┘       └────┘  └─────┘       
pid                  └──┘              
st   ───────────────────────┘└───────────────┘└─
154      cases f b with a b', { exact h },
id                                  
src      └────┘  └────────┘    └────┘ 
typ      └────┘└────────┘    └────┘
doc      └────┘  └────────┘    └────┘ 
txt      └────┘  └────────┘    └────┘ 
par      └────┘  └────────┘    └────┘ 
pid             └────────┘          
st   ──────────────────────┘└──┘└──────┘└┘
155      { contradiction } },
src        └────────────┘
typ        └────────────┘
doc        └────────────┘
txt        └────────────┘
par        └────────────┘
pid                     
st   ───────────────────┘└──┘
156    { rw [stream.corec'_eq (corec.F f) (corec.F f o).2,
id           └──────────────┘              └─────┘  
src      └──┘└──────────────┘         └┘ └─────┘  └────
typ      └──┘└──────────────┘         └┘ └─────┘└────
doc      └──┘                         └┘          └────
txt      └──┘                         └┘          └────
par      └──┘                         └┘          └────
pid        └┘                         └┘          └────
st   ─────────────────────────────────────────────────┘└───
157          stream.corec'_eq (corec.F f) o],
id           └──────────────┘  └─────┘   
src  ───────┘└──────────────┘ └─────┘ └┘ 
typ  ───────┘└──────────────┘ └─────┘└┘
doc  ───────┘                         └┘ 
txt  ───────┘                         └┘ 
par  ───────┘                         └┘ 
pid  ───────┘                         └┘ 
st   ─────────────────────────────────────┘└─
158      exact IH (corec.F f o).2 }
id             └┘  └─────┘  
src      └────┘   └─────┘  └──┘
typ      └────┘└┘ └─────┘└──┘
doc      └────┘            └──┘
txt      └────┘            └──┘
par      └────┘            └──┘
pid                       └─┘
st   ────────────────────────────┘└─
159  end
st   ──┘
160  
161  /-- left map of `⊕` -/
162  def lmap (f : α → β) : α ⊕ γ → β ⊕ γ
id                              
src                                  
typ                             
163  | (sum.inl a) := sum.inl (f a)
id      └─────┘      └─────┘  
src     └─────┘       └─────┘
typ     └─────┘      └─────┘  
164  | (sum.inr b) := sum.inr b
id      └─────┘      └─────┘
src     └─────┘       └─────┘
typ     └─────┘      └─────┘
165  
166  /-- right map of `⊕` -/
167  def rmap (f : β → γ) : α ⊕ β → α ⊕ γ
id                              
src                                  
typ                             
168  | (sum.inl a) := sum.inl a
id      └─────┘      └─────┘
src     └─────┘       └─────┘
typ     └─────┘      └─────┘
169  | (sum.inr b) := sum.inr (f b)
id      └─────┘      └─────┘  
src     └─────┘       └─────┘
typ     └─────┘      └─────┘  
170  attribute [simp] lmap rmap
id                    └──┘ └──┘
src                   └──┘ └──┘
typ                   └──┘ └──┘
doc             └──┘  └──┘ └──┘
171  
172  @[simp] lemma corec_eq (f : β → α ⊕ β) (b : β) :
id                                           
src                                    
typ                                          
doc    └──┘
173    destruct (corec f b) = rmap (corec f) (f b) :=
id     └──────┘  └───┘     └──┘  └───┘     
src    └──────┘  └───┘       └──┘  └───┘
typ    └──────┘  └───┘     └──┘  └───┘     
doc    └──────┘  └───┘        └──┘  └───┘
174  begin
st   └─────
175    dsimp [corec, destruct],
id            └───┘  └──────┘
src    └─────┘└───┘└┘└──────┘
typ    └─────┘└───┘└┘└──────┘
doc    └─────┘└───┘└┘└──────┘
txt    └─────┘     └┘        
par    └─────┘     └┘        
pid              └┘        
st   ────────────────────────┘└─
176    change stream.corec' (corec.F f) (sum.inr b) 0 with corec.F._match_1 (f b),
id            └───────────┘  └─────┘    └─────┘          └──────────────┘   
src    └─────┘└───────────┘ └─────┘ └┘ └─────┘ └───────┘└──────────────┘   
typ    └─────┘└───────────┘ └─────┘└┘ └─────┘└───────┘└──────────────┘ 
doc    └─────┘                      └┘         └───────┘                   
txt    └─────┘                      └┘         └───────┘                   
par    └─────┘                      └┘         └───────┘                   
pid                                └┘         └┘└─────┘                   
st   ───────────────────────────────────────────────────────────────────────────┘└─
177    induction h : f b with a b', { refl },
id                    
src    └────────┘ └─┘  └────────┘    └───┘
typ    └────────┘ └─┘└────────┘    └───┘
doc    └────────┘ └─┘  └────────┘    └───┘
txt    └────────┘ └─┘  └────────┘    └───┘
par    └────────┘ └─┘  └────────┘    └───┘
pid              └─┘  └───────┘        
st   ────────────────────────────┘└──┘└───┘└┘
178    dsimp [corec.F, destruct],
id            └─────┘  └──────┘
src    └─────┘└─────┘└┘└──────┘
typ    └─────┘└─────┘└┘└──────┘
doc    └─────┘       └┘└──────┘
txt    └─────┘       └┘        
par    └─────┘       └┘        
pid                └┘        
st   ──────────────────────────┘└─
179    apply congr_arg, apply subtype.eq,
id           └───────┘        └────────┘
src    └────┘└───────┘  └────┘└────────┘
typ    └────┘└───────┘  └────┘└────────┘
doc    └────┘           └────┘
txt    └────┘           └────┘
par    └────┘           └────┘
pid                         
st   ────────────────┘└────────────────┘└─
180    dsimp [corec, tail],
id            └───┘  └──┘
src    └─────┘└───┘└┘└──┘
typ    └─────┘└───┘└┘└──┘
doc    └─────┘└───┘└┘└──┘
txt    └─────┘     └┘    
par    └─────┘     └┘    
pid              └┘    
st   ────────────────────┘└─
181    rw [stream.corec'_eq, stream.tail_cons],
id         └──────────────┘  └──────────────┘
src    └──┘└──────────────┘└┘└──────────────┘
typ    └──┘└──────────────┘└┘└──────────────┘
doc    └──┘                └┘                
txt    └──┘                └┘                
par    └──┘                └┘                
pid      └┘                └┘                
st   ─────────────────────┘└────────────────┘└──
182    dsimp [corec.F], rw h
id            └─────┘      
src    └─────┘└─────┘  └─┘ 
typ    └─────┘└─────┘  └─┘
doc    └─────┘         └─┘ 
txt    └─────┘         └─┘ 
par    └─────┘         └─┘ 
pid                     
st   ────────────────┘└─────┘
183  end
st   └─┘
184  
185  section bisim
186    variable (R : computation α → computation α → Prop)
id                   └─────────┘     └─────────┘
src                  └─────────┘     └─────────┘
typ                  └─────────┘     └─────────┘
doc                  └─────────┘     └─────────┘
187  
188    local infix ~ := R
189  
190    def bisim_o : α ⊕ computation α → α ⊕ computation α → Prop
id                     └─────────┘     └─────────┘ 
src                     └─────────┘        └─────────┘
typ                    └─────────┘     └─────────┘ 
doc                      └─────────┘         └─────────┘
191    | (sum.inl a) (sum.inl a') := a = a'
id                   └─────┘ └┘       
src                   └─────┘          
typ                  └─────┘ └┘       
192    | (sum.inr s) (sum.inr s') := R s s'
id                   └─────┘ └┘     
src                   └─────┘
typ                  └─────┘ └┘     
193    | _           _            := false
id                                   └───┘
src                                  └───┘
typ                                  └───┘
194    attribute [simp] bisim_o
id                      └─────┘
src                     └─────┘
typ                     └─────┘
doc               └──┘
195  
196    def is_bisimulation := ∀ ⦃s₁ s₂⦄, s₁ ~ s₂ → bisim_o R (destruct s₁) (destruct s₂)
id                               └┘ └┘   └┘  └┘   └─────┘   └──────┘ └┘   └──────┘ └┘
src                                                └─────┘    └──────┘      └──────┘
typ                              └┘ └┘   └┘  └┘   └─────┘   └──────┘ └┘   └──────┘ └┘
doc                                                           └──────┘      └──────┘
197  
198    -- If two computations are bisimilar, then they are equal
199    theorem eq_of_bisim (bisim : is_bisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂ :=
id                                  └─────────────┘                └┘  └┘    └┘  └┘
src                                 └─────────────┘                               
typ                                 └─────────────┘                └┘  └┘    └┘  └┘
200    begin
st     └─────
201      apply subtype.eq,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
202      apply stream.eq_of_bisim (λx y, ∃ s s' : computation α, s.1 = x ∧ s'.1 = y ∧ R s s'),
id             └────────────────┘                └─────────┘                     
src      └────┘└────────────────┘  └───┘└──────┘└─────────┘  └─┘   └─┘       
typ      └────┘└────────────────┘  └───┘└──────┘└─────────┘ └─┘   └─┘      
doc      └────┘                    └───┘ └──────┘└─────────┘   └─┘     └─┘       
txt      └────┘                    └───┘ └──────┘              └─┘     └─┘       
par      └────┘                    └───┘ └──────┘              └─┘     └─┘       
pid                               └───┘ └──────┘              └─┘     └─┘       
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
203      dsimp [stream.is_bisimulation],
id              └────────────────────┘
src      └─────┘└────────────────────┘
typ      └─────┘└────────────────────┘
doc      └─────┘                      
txt      └─────┘                      
par      └─────┘                      
pid                                 
st   ─────────────────────────────────┘└─
204      intros t₁ t₂ e,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ─────────────────┘└─
205      exact match t₁, t₂, e with ._, ._, ⟨s, s', rfl, rfl, r⟩ :=
id                   └┘  └┘                   └┘       └─┘
src      └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘└─┘└┘ └────
typ      └────┘     └┘└┘└┘└┘└────┘  └┘  └┘ └┘└┘└┘   └┘└─┘└┘ └────
doc      └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └┘ └────
txt      └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └┘ └────
par      └────┘       └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └┘ └────
pid                  └┘  └┘ └────┘  └┘  └┘  └┘  └┘   └┘   └┘ └────
st   ───────────────────────────────────────────────────────────────
206        suffices head s = head s' ∧ R (tail s) (tail s'), from
id                           └──┘      
src  ─────┘        └────┘  └──┘          └┘       └───────
typ  ─────┘        └────┘  └──┘         └┘       └───────
doc  ─────┘        └────┘  └──┘          └┘       └───────
txt  ─────┘        └────┘                └┘       └───────
par  ─────┘        └────┘                └┘       └───────
pid  ─────┘        └────┘                └┘       └───────
st   ─────────────────────────────────────────────────────────────
207        and.imp id (λr, ⟨tail s, tail s',
id         └─────┘ └┘               └──┘
src  ─────┘└─────┘└┘  └─┘      └┘└──┘  └─
typ  ─────┘└─────┘└┘  └─┘      └┘└──┘  └─
doc  ─────┘           └─┘      └┘└──┘  └─
txt  ─────┘           └─┘      └┘      └─
par  ─────┘           └─┘      └┘      └─
pid  ─────┘           └─┘      └┘      └─
st   ────────────────────────────────────────
208          by cases s; refl, by cases s'; refl, r⟩) this,
id                                     └┘
src  ───────┘  └────┘ └┘└──┘└┘  └────┘  └┘└──┘└┘ └─┘    └─
typ  ───────┘  └────┘└┘└──┘└┘  └────┘└┘└┘└──┘└┘ └─┘    └─
doc  ───────┘  └────┘ └┘└──┘└┘  └────┘  └┘└──┘└┘ └─┘    └─
txt  ───────┘  └────┘ └┘└──┘└┘  └────┘  └┘└──┘└┘ └─┘    └─
par  ───────┘  └────┘ └┘└──┘└┘  └────┘  └┘└──┘└┘ └─┘    └─
pid  ───────┘  └─────┘ └──────┘  └─────┘  └──────┘ └─┘    └─
st   ─────────┘└────────────┘└──┘└─────────────┘└───────────
209        begin
src  ─────┘     
typ  ─────┘     
doc  ─────┘     
txt  ─────┘     
par  ─────┘     
pid  ─────┘     
st   ─────┘└─────
210          have := bisim r, revert r this,
id                   └───┘ 
src  ───────┘└──────┘      └┘└───────────┘└─
typ  ───────┘└──────┘└───┘└┘└───────────┘└─
doc  ───────┘└──────┘      └┘└───────────┘└─
txt  ───────┘└──────┘      └┘└───────────┘└─
par  ───────┘└──────┘      └┘└───────────┘└─
pid  ───────────────┘      └────────────────
st   ──────────────────────┘└─────────────┘└─
211          apply cases_on s _ _; intros; apply cases_on s' _ _; intros; intros r this,
id                 └──────┘                     └──────┘ └┘
src  ───────┘└────┘└──────┘ └──┘└┘└────┘└┘└────┘└──────┘  └──┘└┘└────┘└┘└───────────┘└─
typ  ─────────────┘└──────┘└────┘└────┘└──────┘└──────┘└┘└────┘└────┘└┘└───────────┘└─
doc  ───────┘└────┘         └──┘└┘└────┘└┘└────┘          └──┘└┘└────┘└┘└───────────┘└─
txt  ───────┘└────┘         └──┘└┘└────┘└┘└────┘          └──┘└┘└────┘└┘└───────────┘└─
par  ─────────────┘         └────┘└────┘└──────┘          └────┘└────┘└┘└───────────┘└─
pid  ─────────────┘         └──────────────────┘          └────────────────────────────
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
212          { constructor, dsimp at this, rw this, assumption },
id                                            └──┘
src  ─────────┘└─────────┘└┘└───────────┘└┘└─┘    └┘└─────────┘└──
typ  ─────────┘└─────────┘└┘└───────────┘└┘└─┘└──┘└┘└─────────┘└──
doc  ─────────┘└─────────┘└┘└───────────┘└┘└─┘    └┘└─────────┘└──
txt  ─────────┘└─────────┘└┘└───────────┘└┘└─┘    └┘└─────────┘└──
par  ─────────┘└─────────┘└┘└───────────┘└┘└─┘    └┘└─────────┘└──
pid  ────────────────────────────────────────┘    └───────────────
st   ────────┘└──────────┘└─────────────┘└───────┘└───────────┘└─
213          { rw [destruct_ret, destruct_think] at this,
id                 └──────────┘  └────────────┘
src  ─────────┘└──┘└──────────┘└┘└────────────┘└───────┘└─
typ  ─────────┘└──┘└──────────┘└┘└────────────┘└───────┘└─
doc  ─────────┘└──┘            └┘              └───────┘└─
txt  ─────────┘└──┘            └┘              └───────┘└─
par  ─────────┘└──┘            └┘              └───────┘└─
pid  ─────────────┘            └┘              └──────────
st   ────────┘└───────────────┘└──────────────┘└──────┘└─
214            exact false.elim this },
id                   └────────┘ └──┘
src  ───────────────┘└────────┘    └───
typ  ───────────────┘└────────┘└──┘└───
doc  ───────────────┘              └───
txt  ───────────────┘              └───
par  ───────────────┘              └───
pid  ───────────────┘              └───
st   ───────────────────────────────┘└─
215          { rw [destruct_ret, destruct_think] at this,
id                 └──────────┘  └────────────┘
src  ─────────┘└──┘└──────────┘└┘└────────────┘└───────┘└─
typ  ─────────┘└──┘└──────────┘└┘└────────────┘└───────┘└─
doc  ─────────┘└──┘            └┘              └───────┘└─
txt  ─────────┘└──┘            └┘              └───────┘└─
par  ─────────┘└──┘            └┘              └───────┘└─
pid  ─────────────┘            └┘              └──────────
st   ────────┘└───────────────┘└──────────────┘└──────┘└─
216            exact false.elim this },
id                   └────────┘ └──┘
src  ───────────────┘└────────┘    └───
typ  ───────────────┘└────────┘└──┘└───
doc  ───────────────┘              └───
txt  ───────────────┘              └───
par  ───────────────┘              └───
pid  ───────────────┘              └───
st   ───────────────────────────────┘└─
217          { simp at this, simp [*] }
src  ─────────┘└──────────┘└┘└───────┘└─
typ  ─────────┘└──────────┘└┘└───────┘└─
doc  ─────────┘└──────────┘└┘└───────┘└─
txt  ─────────┘└──────────┘└┘└───────┘└─
par  ─────────┘└──────────┘└┘└───────┘└─
pid  ───────────────────────────────────
st   ─────────────────────┘└─────────┘└─
218        end
src  ──────────
typ  ──────────
doc  ──────────
txt  ──────────
par  ──────────
pid  ──────────
st   ────────┘
219      end,
src  ──────┘
typ  ──────┘
doc  ──────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ──────┘└─
220      exact ⟨s₁, s₂, rfl, rfl, r⟩
id              └┘  └┘       └─┘  
src      └────┘   └┘  └┘   └┘└─┘└┘ └─
typ      └────┘ └┘└┘└┘└┘   └┘└─┘└┘└─
doc      └────┘   └┘  └┘   └┘   └┘ └─
txt      └────┘   └┘  └┘   └┘   └┘ └─
par      └────┘   └┘  └┘   └┘   └┘ └─
pid              └┘  └┘   └┘   └┘ 
st   ────────────────────────────────
221    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
222  end bisim
223  
224  -- It's more of a stretch to use ∈ for this relation, but it
225  -- asserts that the computation limits to the given value.
226  protected def mem (a : α) (s : computation α) := some a ∈ s.1
id                                 └─────────┘      └──┘   
src                                 └─────────┘       └──┘     
typ                                └─────────┘      └──┘   
doc                                 └─────────┘
227  
228  instance : has_mem α (computation α) := ⟨computation.mem⟩
id              └─────┘   └─────────┘       └─────────────┘
src             └─────┘    └─────────┘        └─────────────┘
typ             └─────┘   └─────────┘       └─────────────┘
doc                        └─────────┘
229  
230  theorem le_stable (s : computation α) {a m n} (h : m ≤ n) :
id                          └─────────┘                  
src                         └─────────┘                   
typ                         └─────────┘                  
doc                         └─────────┘
231    s.1 m = some a → s.1 n = some a :=
id         └──┘        └──┘ 
src          └──┘           └──┘
typ        └──┘        └──┘ 
232  by {cases s with f al, induction h with n h IH, exacts [id, λ h2, al (IH h2)]}
id                                                         └┘        └┘  └┘
src      └────┘ └────────┘  └────────┘ └──────────┘  └──────┘└┘└┘ └───┘       └┘
typ      └────┘└────────┘  └────────┘└──────────┘  └──────┘└┘└┘ └───┘└┘ └┘  └┘
doc      └────┘ └────────┘  └────────┘ └──────────┘  └──────┘  └┘ └───┘       └┘
txt      └────┘ └────────┘  └────────┘ └──────────┘  └──────┘  └┘ └───┘       └┘
par      └────┘ └────────┘  └────────┘ └──────────┘  └──────┘  └┘ └───┘       └┘
pid            └────────┘            └─────────┘        └┘  └┘ └───┘       └┘
st     └─────────────────┘└───────────────────────┘└─────────────────────────────┘└┘
233  
234  theorem mem_unique :
235     relator.left_unique ((∈) : α → computation α → Prop) :=
id      └─────────────────┘          └─────────┘ 
src     └─────────────────┘           └─────────┘
typ     └─────────────────┘          └─────────┘ 
doc                                    └─────────┘
236  λa s b ⟨m, ha⟩ ⟨n, hb⟩, by injection
id              
src                             └─────────
typ                        └─────────
doc                             └─────────
txt                             └─────────
par                             └─────────
pid                                      
st                             └──────────
237    (le_stable s (le_max_left m n) ha.symm).symm.trans
id                   └─────────┘      └─────┘
src  ─┘            └─────────┘  └┘└─────┘└────────────
typ  ─┘            └─────────┘  └┘└─────┘└────────────
doc  ─┘                         └┘       └────────────
txt  ─┘                         └┘       └────────────
par  ─┘                         └┘       └────────────
pid  ─┘                         └┘       └────────────
st   ─────────────────────────────────────────────────────
238    (le_stable s (le_max_right m n) hb.symm)
id      └───────┘   └──────────┘    └─────┘
src  ─┘ └───────┘  └──────────┘  └┘└─────┘└─
typ  ─┘ └───────┘ └──────────┘└┘└─────┘└─
doc  ─┘                          └┘       └─
txt  ─┘                          └┘       └─
par  ─┘                          └┘       └─
pid  ─┘                          └┘       
st   ───────────────────────────────────────────
239  
src  
typ  
doc  
txt  
par  
pid  
st   
240  /-- `terminates s` asserts that the computation `s` eventually terminates with some value. -/
241  @[class] def terminates (s : computation α) : Prop := ∃ a, a ∈ s
id                                └─────────┘                 
src                               └─────────┘                   
typ                               └─────────┘                 
doc                               └─────────┘
242  
243  theorem terminates_of_mem {s : computation α} {a : α} : a ∈ s → terminates s :=
id                                  └─────────┘                 └────────┘ 
src                                 └─────────┘                     └────────┘
typ                                 └─────────┘                 └────────┘ 
doc                                 └─────────┘                      └────────┘
244  exists.intro a
id   └──────────┘ 
src  └──────────┘
typ  └──────────┘ 
245  
246  theorem terminates_def (s : computation α) : terminates s ↔ ∃ n, (s.1 n).is_some :=
id                               └─────────┘     └────────┘         └─────┘
src                              └─────────┘      └────────┘             └─────┘
typ                              └─────────┘     └────────┘         └─────┘
doc                              └─────────┘      └────────┘
247  ⟨λ⟨a, n, h⟩, ⟨n, by {dsimp [stream.nth] at h, rw ←h, exact rfl}⟩,
id                             └────────┘                    └─┘
src                       └─────┘└────────┘└────┘  └──┘   └────┘└─┘
typ                     └─────┘└────────┘└────┘  └──┘  └────┘└─┘
doc                       └─────┘          └────┘  └──┘   └────┘
txt                       └─────┘          └────┘  └──┘   └────┘
par                       └─────┘          └────┘  └──┘   └────┘
pid                                      └──┘    └┘        
st                      └───────────────────────┘└─────┘└─────────┘└┘
248  λ⟨n, h⟩, ⟨option.get h, n, (option.eq_some_of_is_some h).symm⟩⟩
id          └────────┘        └───────────────────────┘   └──┘
src            └────────┘        └───────────────────────┘   └──┘
typ         └────────┘        └───────────────────────┘   └──┘
249  
250  theorem ret_mem (a : α) : a ∈ return a :=
id                              └────┘ 
src                               └────┘
typ                             └────┘ 
doc                                └────┘
251  exists.intro 0 rfl
id   └──────────┘   └─┘
src  └──────────┘   └─┘
typ  └──────────┘   └─┘
252  
253  theorem eq_of_ret_mem {a a' : α} (h : a' ∈ return a) : a' = a :=
id                                        └┘  └────┘     └┘  
src                                            └────┘         
typ                                       └┘  └────┘     └┘  
doc                                             └────┘
254  mem_unique h (ret_mem _)
id   └────────┘   └─────┘
src  └────────┘    └─────┘
typ  └────────┘   └─────┘
255  
256  instance ret_terminates (a : α) : terminates (return a) :=
id                                    └────────┘  └────┘ 
src                                    └────────┘  └────┘
typ                                   └────────┘  └────┘ 
doc                                    └────────┘  └────┘
257  terminates_of_mem (ret_mem _)
id   └───────────────┘  └─────┘
src  └───────────────┘  └─────┘
typ  └───────────────┘  └─────┘
258  
259  theorem think_mem {s : computation α} {a} : a ∈ s → a ∈ think s
id                          └─────────┘               └───┘ 
src                         └─────────┘                    └───┘
typ                         └─────────┘               └───┘ 
doc                         └─────────┘                      └───┘
260  | ⟨n, h⟩ := ⟨n+1, h⟩
id               
src                
typ              
261  
262  instance think_terminates (s : computation α) :
id                                  └─────────┘ 
src                                 └─────────┘
typ                                 └─────────┘ 
doc                                 └─────────┘
263    ∀ [terminates s], terminates (think s)
id       └────────┘    └────────┘  └───┘ 
src       └────────┘     └────────┘  └───┘
typ      └────────┘    └────────┘  └───┘ 
doc       └────────┘     └────────┘  └───┘
264  | ⟨a, n, h⟩ := ⟨a, n+1, h⟩
id                    
src                      
typ                   
265  
266  theorem of_think_mem {s : computation α} {a} : a ∈ think s → a ∈ s
id                             └─────────┘           └───┘     
src                            └─────────┘             └───┘       
typ                            └─────────┘           └───┘     
doc                            └─────────┘              └───┘
267  | ⟨n, h⟩ := by {cases n with n', contradiction, exact ⟨n', h⟩}
id                                                         └┘  
src                  └────┘ └──────┘  └───────────┘  └────┘   └┘ 
typ                  └────┘└──────┘  └───────────┘  └────┘ └┘└┘
doc                  └────┘ └──────┘  └───────────┘  └────┘   └┘ 
txt                  └────┘ └──────┘  └───────────┘  └────┘   └┘ 
par                  └────┘ └──────┘  └───────────┘  └────┘   └┘ 
pid                        └──────┘                         └┘ 
st                 └───────────────┘└─────────────┘└─────────────┘└┘
268  
269  theorem of_think_terminates {s : computation α} :
id                                    └─────────┘ 
src                                   └─────────┘
typ                                   └─────────┘ 
doc                                   └─────────┘
270    terminates (think s) → terminates s
id     └────────┘  └───┘    └────────┘ 
src    └────────┘  └───┘      └────────┘
typ    └────────┘  └───┘    └────────┘ 
doc    └────────┘  └───┘      └────────┘
271  | ⟨a, h⟩ := ⟨a, of_think_mem h⟩
id                 └──────────┘
src                  └──────────┘
typ                └──────────┘
272  
273  theorem not_mem_empty (a : α) : a ∉ empty α :=
id                                    └───┘ 
src                                     └───┘
typ                                   └───┘ 
doc                                      └───┘
274  λ ⟨n, h⟩, by clear _fun_match; contradiction
id     
src               └──────────────┘  └─────────────
typ              └──────────────┘  └─────────────
doc               └──────────────┘  └─────────────
txt               └──────────────┘  └─────────────
par               └──────────────┘  └─────────────
pid                    └─────────┘               
st               └────────────────────────────────
275  
src  
typ  
doc  
txt  
par  
pid  
st   
276  theorem not_terminates_empty : ¬ terminates (empty α) :=
id                                   └────────┘  └───┘ 
src                                  └────────┘  └───┘
typ                                  └────────┘  └───┘ 
doc                                   └────────┘  └───┘
277  λ ⟨a, h⟩, not_mem_empty a h
id          └───────────┘
src            └───────────┘
typ         └───────────┘
278  
279  theorem eq_empty_of_not_terminates {s} (H : ¬ terminates s) : s = empty α :=
id                                                └────────┘       └───┘ 
src                                               └────────┘         └───┘
typ                                               └────────┘       └───┘ 
doc                                                └────────┘          └───┘
280  begin
st   └─────
281    apply subtype.eq, funext n,
id           └────────┘
src    └────┘└────────┘  └──────┘
typ    └────┘└────────┘  └──────┘
doc    └────┘            └──────┘
txt    └────┘            └──────┘
par    └────┘            └──────┘
pid                           └┘
st   ─────────────────┘└────────┘└─
282    induction h : s.val n, {refl},
id                   └───┘ 
src    └────────┘ └─┘└───┘    └──┘
typ    └────────┘ └─┘└───┘   └──┘
doc    └────────┘ └─┘         └──┘
txt    └────────┘ └─┘         └──┘
par    └────────┘ └─┘         └──┘
pid              └─┘     
st   ──────────────────────┘└─────┘└┘
283    refine absurd _ H, exact ⟨_, _, h.symm⟩
id            └────┘                  └────┘
src    └─────┘└────┘└─┘   └────┘ └────┘└────┘└┘
typ    └─────┘└────┘└─┘  └────┘ └────┘└────┘└┘
doc    └─────┘      └─┘   └────┘ └────┘      └┘
txt    └─────┘      └─┘   └────┘ └────┘      └┘
par    └─────┘      └─┘   └────┘ └────┘      └┘
pid                └─┘         └────┘      
st   ──────────────────┘└─────────────────────┘
284  end
st   └─┘
285  
286  theorem thinkN_mem {s : computation α} {a} : ∀ n, a ∈ thinkN s n ↔ a ∈ s
id                           └─────────┘               └────┘      
src                          └─────────┘                  └────┘        
typ                          └─────────┘               └────┘      
doc                          └─────────┘                   └────┘
287  | 0 := iff.rfl
id          └─────┘
src         └─────┘
typ         └─────┘
288  | (n+1) := iff.trans ⟨of_think_mem, think_mem⟩ (thinkN_mem n)
id            └───────┘  └──────────┘  └───────┘   └────────┘
src            └───────┘  └──────────┘  └───────┘
typ           └───────┘  └──────────┘  └───────┘   └────────┘
289  
290  instance thinkN_terminates (s : computation α) :
id                                   └─────────┘ 
src                                  └─────────┘
typ                                  └─────────┘ 
doc                                  └─────────┘
291    ∀ [terminates s] n, terminates (thinkN s n)
id       └────────┘     └────────┘  └────┘  
src       └────────┘       └────────┘  └────┘
typ      └────────┘     └────────┘  └────┘  
doc       └────────┘       └────────┘  └────┘
292  | ⟨a, h⟩ n := ⟨a, (thinkN_mem n).2 h⟩
id                   └────────┘   
src                     └────────┘   
typ                  └────────┘   
293  
294  theorem of_thinkN_terminates (s : computation α) (n) :
id                                     └─────────┘ 
src                                    └─────────┘
typ                                    └─────────┘ 
doc                                    └─────────┘
295    terminates (thinkN s n) → terminates s
id     └────────┘  └────┘     └────────┘ 
src    └────────┘  └────┘        └────────┘
typ    └────────┘  └────┘     └────────┘ 
doc    └────────┘  └────┘        └────────┘
296  | ⟨a, h⟩ := ⟨a, (thinkN_mem _).1 h⟩
id                  └────────┘   
src                   └────────┘   
typ                 └────────┘   
297  
298  /-- `promises s a`, or `s ~> a`, asserts that although the computation `s`
299    may not terminate, if it does, then the result is `a`. -/
300  def promises (s : computation α) (a : α) : Prop := ∀ ⦃a'⦄, a' ∈ s → a = a'
id                     └─────────┘                       └┘   └┘       └┘
src                    └─────────┘                                        
typ                    └─────────┘                       └┘   └┘       └┘
doc                    └─────────┘
301  
302  infix ` ~> `:50 := promises
id                      └──────┘
src                     └──────┘
typ                     └──────┘
doc                     └──────┘
303  
304  theorem mem_promises {s : computation α} {a : α} : a ∈ s → s ~> a :=
id                             └─────────┘                  └┘ 
src                            └─────────┘                       └┘
typ                            └─────────┘                  └┘ 
doc                            └─────────┘                        └┘
305  λ h a', mem_unique h
id      └┘  └────────┘ 
src          └────────┘
typ     └┘  └────────┘ 
306  
307  theorem empty_promises (a : α) : empty α ~> a :=
id                                   └───┘  └┘ 
src                                   └───┘   └┘
typ                                  └───┘  └┘ 
doc                                   └───┘   └┘
308  λ a' h, absurd h (not_mem_empty _)
id     └┘   └────┘   └───────────┘
src          └────┘    └───────────┘
typ    └┘   └────┘   └───────────┘
309  
310  section get
311  variables (s : computation α) [h : terminates s]
id                  └─────────┘         └────────┘
src                 └─────────┘         └────────┘
typ                 └─────────┘         └────────┘
doc                 └─────────┘         └────────┘
312  include s h
313  
314  /-- `length s` gets the number of steps of a terminating computation -/
315  def length : ℕ := nat.find ((terminates_def _).1 h)
id                    └──────┘   └────────────┘     
src                   └──────┘   └────────────┘   
typ                   └──────┘   └────────────┘     
316  
317  /-- `get s` returns the result of a terminating computation -/
318  def get : α := option.get (nat.find_spec $ (terminates_def _).1 h)
id                 └────────┘  └───────────┘    └────────────┘     
src                 └────────┘  └───────────┘    └────────────┘   
typ                └────────┘  └───────────┘    └────────────┘     
319  
320  theorem get_mem : get s ∈ s :=
id                     └─┘   
src                    └─┘   
typ                    └─┘   
doc                    └─┘
321  exists.intro (length s) (option.eq_some_of_is_some _).symm
id   └──────────┘  └────┘    └───────────────────────┘   └──┘
src  └──────────┘  └────┘     └───────────────────────┘   └──┘
typ  └──────────┘  └────┘    └───────────────────────┘   └──┘
doc                └────┘
322  
323  theorem get_eq_of_mem {a} : a ∈ s → get s = a :=
id                                    └─┘   
src                                     └─┘   
typ                                   └─┘   
doc                                      └─┘
324  mem_unique (get_mem _)
id   └────────┘  └─────┘
src  └────────┘  └─────┘
typ  └────────┘  └─────┘
325  
326  theorem mem_of_get_eq {a} : get s = a → a ∈ s :=
id                               └─┘        
src                              └─┘          
typ                              └─┘        
doc                              └─┘
327  by intro h; rw ←h; apply get_mem
id                           └─────┘
src     └─────┘  └──┘   └────┘└─────┘
typ     └─────┘  └──┘  └────┘└─────┘
doc     └─────┘  └──┘   └────┘       
txt     └─────┘  └──┘   └────┘       
par     └─────┘  └──┘   └────┘       
pid          └┘    └┘               
st     └──────────────────────────────
328  
src  
typ  
doc  
txt  
par  
pid  
st   
329  @[simp] theorem get_think : get (think s) = get s :=
id                               └─┘  └───┘    └─┘ 
src                              └─┘  └───┘     └─┘
typ                              └─┘  └───┘    └─┘ 
doc    └──┘                      └─┘  └───┘      └─┘
330  get_eq_of_mem _ $ let ⟨n, h⟩ := get_mem s in ⟨n+1, h⟩
id   └───────────┘     └─┘         └─────┘       
src  └───────────┘                   └─────┘        
typ  └───────────┘     └─┘         └─────┘       
331  
332  @[simp] theorem get_thinkN (n) : get (thinkN s n) = get s :=
id                                    └─┘  └────┘     └─┘ 
src                                   └─┘  └────┘       └─┘
typ                                   └─┘  └────┘     └─┘ 
doc    └──┘                           └─┘  └────┘        └─┘
333  get_eq_of_mem _ $ (thinkN_mem _).2 (get_mem _)
id   └───────────┘      └────────┘      └─────┘
src  └───────────┘      └────────┘      └─────┘
typ  └───────────┘      └────────┘      └─────┘
334  
335  theorem get_promises : s ~> get s := λ a, get_eq_of_mem _
id                           └┘ └─┘         └───────────┘
src                           └┘ └─┘           └───────────┘
typ                          └┘ └─┘         └───────────┘
doc                           └┘ └─┘
336  
337  theorem mem_of_promises {a} (p : s ~> a) : a ∈ s :=
id                                     └┘       
src                                     └┘        
typ                                    └┘       
doc                                     └┘
338  by unfreezeI; cases h with a' h; rw p h; exact h
id                                               
src     └───────┘  └────┘ └────────┘  └─┘    └────┘ 
typ     └───────┘  └────┘└────────┘  └─┘  └────┘
doc     └───────┘  └────┘ └────────┘  └─┘    └────┘ 
txt     └───────┘  └────┘ └────────┘  └─┘    └────┘ 
par     └───────┘  └────┘ └────────┘  └─┘    └────┘ 
pid                      └────────┘              
st     └────────────────────────────────┘└───────────
339  
src  
typ  
doc  
txt  
par  
pid  
st   
340  theorem get_eq_of_promises {a} : s ~> a → get s = a :=
id                                     └┘    └─┘   
src                                     └┘     └─┘   
typ                                    └┘    └─┘   
doc                                     └┘     └─┘
341  get_eq_of_mem _ ∘ mem_of_promises _
id   └───────────┘    └─────────────┘
src  └───────────┘    └─────────────┘
typ  └───────────┘    └─────────────┘
342  
343  end get
344  
345  /-- `results s a n` completely characterizes a terminating computation:
346    it asserts that `s` terminates after exactly `n` steps, with result `a`. -/
347  def results (s : computation α) (a : α) (n : ℕ) :=
id                    └─────────┘               
src                   └─────────┘                 
typ                   └─────────┘               
doc                   └─────────┘
348  ∃ (h : a ∈ s), @length _ s (terminates_of_mem h) = n
id              └────┘     └───────────────┘    
src               └────┘      └───────────────┘    
typ             └────┘     └───────────────┘    
doc                  └────┘
349  
350  theorem results_of_terminates (s : computation α) [T : terminates s] :
id                                      └─────────┘        └────────┘ 
src                                     └─────────┘         └────────┘
typ                                     └─────────┘        └────────┘ 
doc                                     └─────────┘         └────────┘
351    results s (get s) (length s) :=
id     └─────┘   └─┘    └────┘ 
src    └─────┘    └─┘     └────┘
typ    └─────┘   └─┘    └────┘ 
doc    └─────┘    └─┘     └────┘
352  ⟨get_mem _, rfl⟩
id    └─────┘    └─┘
src   └─────┘    └─┘
typ   └─────┘    └─┘
353  
354  theorem results_of_terminates' (s : computation α) [T : terminates s] {a} (h : a ∈ s) :
id                                       └─────────┘        └────────┘              
src                                      └─────────┘         └────────┘               
typ                                      └─────────┘        └────────┘              
doc                                      └─────────┘         └────────┘
355    results s a (length s) :=
id     └─────┘    └────┘ 
src    └─────┘      └────┘
typ    └─────┘    └────┘ 
doc    └─────┘      └────┘
356  by rw ←get_eq_of_mem _ h; apply results_of_terminates
id          └───────────┘           └───────────────────┘
src     └──┘└───────────┘└─┘   └────┘└───────────────────┘
typ     └──┘└───────────┘└─┘  └────┘└───────────────────┘
doc     └──┘             └─┘   └────┘                     
txt     └──┘             └─┘   └────┘                     
par     └──┘             └─┘   └────┘                     
pid       └┘             └─┘                             
st     └───────────────────────────────────────────────────
357  
src  
typ  
doc  
txt  
par  
pid  
st   
358  theorem results.mem {s : computation α} {a n} : results s a n → a ∈ s
id                            └─────────┘           └─────┘       
src                           └─────────┘            └─────┘           
typ                           └─────────┘           └─────┘       
doc                           └─────────┘            └─────┘
359  | ⟨m, _⟩ := m
id      
typ     
360  
361  theorem results.terminates {s : computation α} {a n} (h : results s a n) : terminates s :=
id                                   └─────────┘              └─────┘       └────────┘ 
src                                  └─────────┘               └─────┘          └────────┘
typ                                  └─────────┘              └─────┘       └────────┘ 
doc                                  └─────────┘               └─────┘          └────────┘
362  terminates_of_mem h.mem
id   └───────────────┘ └──┘
src  └───────────────┘  └──┘
typ  └───────────────┘ └──┘
363  
364  theorem results.length {s : computation α} {a n} [T : terminates s] :
id                               └─────────┘              └────────┘ 
src                              └─────────┘               └────────┘
typ                              └─────────┘              └────────┘ 
doc                              └─────────┘               └────────┘
365    results s a n → length s = n
id     └─────┘     └────┘   
src    └─────┘         └────┘   
typ    └─────┘     └────┘   
doc    └─────┘         └────┘
366  | ⟨_, h⟩ := h
id         
typ        
367  
368  theorem results.val_unique {s : computation α} {a b m n}
id                                   └─────────┘ 
src                                  └─────────┘
typ                                  └─────────┘ 
doc                                  └─────────┘
369    (h1 : results s a m) (h2 : results s b n) : a = b :=
id           └─────┘           └─────┘         
src          └─────┘              └─────┘            
typ          └─────┘           └─────┘         
doc          └─────┘              └─────┘
370  mem_unique h1.mem h2.mem
id   └────────┘ └┘└──┘ └┘└──┘
src  └────────┘   └──┘   └──┘
typ  └────────┘ └┘└──┘ └┘└──┘
371  
372  theorem results.len_unique {s : computation α} {a b m n}
id                                   └─────────┘ 
src                                  └─────────┘
typ                                  └─────────┘ 
doc                                  └─────────┘
373    (h1 : results s a m) (h2 : results s b n) : m = n :=
id           └─────┘           └─────┘         
src          └─────┘              └─────┘            
typ          └─────┘           └─────┘         
doc          └─────┘              └─────┘
374  by haveI := h1.terminates; haveI := h2.terminates; rw [←h1.length, h2.length]
id               └───────────┘           └───────────┘
src     └───────┘└───────────┘  └───────┘└───────────┘  └───┘         └┘         └─
typ     └───────┘└───────────┘  └───────┘└───────────┘  └───┘└───────┘└┘└───────┘└─
doc     └───────┘               └───────┘               └───┘         └┘         └─
txt     └───────┘               └───────┘               └───┘         └┘         └─
par     └───────┘               └───────┘               └───┘         └┘         └─
pid          └─┘                    └─┘                 └─┘         └┘         
st     └───────────────────────────────────────────────────┘└────────┘└─────────┘
375  
src  
typ  
doc  
txt  
par  
pid  
st   
376  theorem exists_results_of_mem {s : computation α} {a} (h : a ∈ s) : ∃ n, results s a n :=
id                                      └─────────┘                    └─────┘   
src                                     └─────────┘                        └─────┘
typ                                     └─────────┘                    └─────┘   
doc                                     └─────────┘                           └─────┘
377  by haveI := terminates_of_mem h; exact ⟨_, results_of_terminates' s h⟩
id               └───────────────┘             └────────────────────┘  
src     └───────┘└───────────────┘   └────┘ └─┘└────────────────────┘  └─
typ     └───────┘└───────────────┘  └────┘ └─┘└────────────────────┘└─
doc     └───────┘                    └────┘ └─┘                        └─
txt     └───────┘                    └────┘ └─┘                        └─
par     └───────┘                    └────┘ └─┘                        └─
pid          └─┘                          └─┘                        
st     └────────────────────────────────────────────────────────────────────
378  
src  
typ  
doc  
txt  
par  
pid  
st   
379  @[simp] theorem get_ret (a : α) : get (return a) = a :=
id                                    └─┘  └────┘    
src                                    └─┘  └────┘    
typ                                   └─┘  └────┘    
doc    └──┘                            └─┘  └────┘
380  get_eq_of_mem _ ⟨0, rfl⟩
id   └───────────┘       └─┘
src  └───────────┘       └─┘
typ  └───────────┘       └─┘
381  
382  @[simp] theorem length_ret (a : α) : length (return a) = 0 :=
id                                       └────┘  └────┘   
src                                       └────┘  └────┘    
typ                                      └────┘  └────┘   
doc    └──┘                               └────┘  └────┘
383  let h := computation.ret_terminates a in
id           └────────────────────────┘ 
src           └────────────────────────┘
typ          └────────────────────────┘ 
384  nat.eq_zero_of_le_zero $ nat.find_min' ((terminates_def (return a)).1 h) rfl
id   └────────────────────┘   └───────────┘   └────────────┘  └────┘       └─┘
src  └────────────────────┘   └───────────┘   └────────────┘  └────┘         └─┘
typ  └────────────────────┘   └───────────┘   └────────────┘  └────┘       └─┘
doc                                                           └────┘
385  
386  theorem results_ret (a : α) : results (return a) a 0 :=
id                                └─────┘  └────┘   
src                                └─────┘  └────┘
typ                               └─────┘  └────┘   
doc                                └─────┘  └────┘
387  ⟨_, length_ret _⟩
id       └────────┘
src      └────────┘
typ      └────────┘
388  
389  @[simp] theorem length_think (s : computation α) [h : terminates s] :
id                                     └─────────┘        └────────┘ 
src                                    └─────────┘         └────────┘
typ                                    └─────────┘        └────────┘ 
doc    └──┘                            └─────────┘         └────────┘
390    length (think s) = length s + 1 :=
id     └────┘  └───┘    └────┘  
src    └────┘  └───┘     └────┘   
typ    └────┘  └───┘    └────┘  
doc    └────┘  └───┘      └────┘
391  begin
st   └─────
392    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
393    { exact nat.find_min' _ (nat.find_spec ((terminates_def _).1 h)) },
id             └───────────┘    └───────────┘   └────────────┘      
src      └────┘└───────────┘└─┘ └───────────┘  └────────────┘└────┘ └─┘
typ      └────┘└───────────┘└─┘ └───────────┘  └────────────┘└────┘└─┘
doc      └────┘             └─┘                              └────┘ └─┘
txt      └────┘             └─┘                              └────┘ └─┘
par      └────┘             └─┘                              └────┘ └─┘
pid                        └─┘                              └────┘ └┘
st   ───┘└─────────────────────────────────────────────────────────────┘└┘
394    { have : (option.is_some ((think s).val (length (think s))) : Prop) :=
id               └────────────┘                 └────┘  └───┘ 
src      └─────┘ └────────────┘        └────┘ └────┘ └───┘ └────┘    └────
typ      └─────┘ └────────────┘        └────┘ └────┘ └───┘└────┘    └────
doc      └─────┘                       └────┘ └────┘ └───┘ └────┘    └────
txt      └─────┘                       └────┘              └────┘    └────
par      └─────┘                       └────┘              └────┘    └────
pid      └───┘└┘                       └────┘              └────┘    └───
st   ─────────────────────────────────────────────────────────────────────────
395        nat.find_spec ((terminates_def _).1 s.think_terminates),
id         └───────────┘   └────────────┘      └────────────────┘
src  ─────┘└───────────┘  └────────────┘└────┘└────────────────┘
typ  ─────┘└───────────┘  └────────────┘└────┘└────────────────┘
doc  ─────┘                             └────┘                  
txt  ─────┘                             └────┘                  
par  ─────┘                             └────┘                  
pid  ─────┘                             └────┘                  
st   ────────────────────────────────────────────────────────────┘└─
396      cases length (think s) with n,
id             └────┘  └───┘ 
src      └────┘└────┘ └───┘ └──────┘
typ      └────┘└────┘ └───┘└──────┘
doc      └────┘└────┘ └───┘ └──────┘
txt      └────┘             └──────┘
par      └────┘             └──────┘
pid                        └─────┘
st   ────────────────────────────────┘└─
397      { contradiction },
src        └────────────┘
typ        └────────────┘
doc        └────────────┘
txt        └────────────┘
par        └────────────┘
pid                     
st   ─────┘└────────────┘└┘
398      { apply nat.succ_le_succ, apply nat.find_min', apply this } }
id               └──────────────┘        └───────────┘
src        └────┘└──────────────┘  └────┘└───────────┘  └────┘    
typ        └────┘└──────────────┘  └────┘└───────────┘  └────┘    
doc        └────┘                  └────┘               └────┘    
txt        └────┘                  └────┘               └────┘    
par        └────┘                  └────┘               └────┘    
pid                                                            
st   ───────────────────────────┘└───────────────────┘└───────────┘└───
399  end
st   ──┘
400  
401  theorem results_think {s : computation α} {a n}
id                              └─────────┘ 
src                             └─────────┘
typ                             └─────────┘ 
doc                             └─────────┘
402    (h : results s a n) : results (think s) a (n + 1) :=
id          └─────┘       └─────┘  └───┘      
src         └─────┘          └─────┘  └───┘         
typ         └─────┘       └─────┘  └───┘      
doc         └─────┘          └─────┘  └───┘
403  by haveI := h.terminates; exact ⟨think_mem h.mem, by rw [length_think, h.length]⟩
id               └──────────┘         └───────┘ └───┘         └──────────┘
src     └───────┘└──────────┘  └────┘ └───────┘└───┘└┘  └──┘└──────────┘└┘        └─
typ     └───────┘└──────────┘  └────┘ └───────┘└───┘└┘  └──┘└──────────┘└┘└──────┘└─
doc     └───────┘              └────┘               └┘  └──┘            └┘        └─
txt     └───────┘              └────┘               └┘  └──┘            └┘        └─
par     └───────┘              └────┘               └┘  └──┘            └┘        └─
pid          └─┘                                  └┘  └───┘            └┘        └┘
st     └────────────────────────────────────────────────┘└───────────────┘└────────┘└─
404  
src  
typ  
doc  
txt  
par  
pid  
st   
405  theorem of_results_think {s : computation α} {a n}
id                                 └─────────┘ 
src                                └─────────┘
typ                                └─────────┘ 
doc                                └─────────┘
406    (h : results (think s) a n) : ∃ m, results s a m ∧ n = m + 1 :=
id          └─────┘  └───┘          └─────┘        
src         └─────┘  └───┘              └─────┘             
typ         └─────┘  └───┘          └─────┘        
doc         └─────┘  └───┘                └─────┘
407  begin
st   └─────
408    haveI := of_think_terminates h.terminates,
id              └─────────────────┘ └──────────┘
src    └───────┘└─────────────────┘└──────────┘
typ    └───────┘└─────────────────┘└──────────┘
doc    └───────┘                   
txt    └───────┘                   
par    └───────┘                   
pid         └─┘                   
st   ──────────────────────────────────────────┘└─
409    have := results_of_terminates' _ (of_think_mem h.mem),
id             └────────────────────┘    └──────────┘ └───┘
src    └──────┘└────────────────────┘└─┘ └──────────┘└───┘
typ    └──────┘└────────────────────┘└─┘ └──────────┘└───┘
doc    └──────┘                      └─┘                  
txt    └──────┘                      └─┘                  
par    └──────┘                      └─┘                  
pid    └───┘└─┘                      └─┘                  
st   ──────────────────────────────────────────────────────┘└─
410    exact ⟨_, this, results.len_unique h (results_think this)⟩,
id                     └────────────────┘   └───────────┘ └──┘
src    └────┘ └─┘    └┘└────────────────┘  └───────────┘    └┘
typ    └────┘ └─┘    └┘└────────────────┘ └───────────┘└──┘└┘
doc    └────┘ └─┘    └┘                                     └┘
txt    └────┘ └─┘    └┘                                     └┘
par    └────┘ └─┘    └┘                                     └┘
pid          └─┘    └┘                                     └┘
st   ───────────────────────────────────────────────────────────┘└─
411  end
st   ──┘
412  
413  @[simp] theorem results_think_iff {s : computation α} {a n} :
id                                          └─────────┘ 
src                                         └─────────┘
typ                                         └─────────┘ 
doc    └──┘                                 └─────────┘
414    results (think s) a (n + 1) ↔ results s a n :=
id     └─────┘  └───┘           └─────┘   
src    └─────┘  └───┘              └─────┘
typ    └─────┘  └───┘           └─────┘   
doc    └─────┘  └───┘                └─────┘
415  ⟨λ h, let ⟨n', r, e⟩ := of_results_think h in by injection e with h'; rwa h',
id        └─┘               └──────────────┘                                └┘
src                          └──────────────┘         └────────┘ └──────┘  └──┘
typ       └─┘               └──────────────┘        └────────┘└──────┘  └──┘└┘
doc                                                   └────────┘ └──────┘  └──┘
txt                                                   └────────┘ └──────┘  └──┘
par                                                   └────────┘ └──────┘  └──┘
pid                                                             └──────┘     
st                                                   └────────────────────────┘└┘
416  results_think⟩
id   └───────────┘
src  └───────────┘
typ  └───────────┘
417  
418  theorem results_thinkN {s : computation α} {a m} :
id                               └─────────┘ 
src                              └─────────┘
typ                              └─────────┘ 
doc                              └─────────┘
419    ∀ n, results s a m → results (thinkN s n) a (m + n)
id         └─────┘      └─────┘  └────┘        
src         └─────┘         └─────┘  └────┘           
typ        └─────┘      └─────┘  └────┘        
doc         └─────┘         └─────┘  └────┘
420  | 0     h := h
id           
typ          
421  | (n+1) h := results_think (results_thinkN n h)
id             └───────────┘  └────────────┘
src              └───────────┘
typ            └───────────┘  └────────────┘
422  
423  theorem results_thinkN_ret (a : α) (n) : results (thinkN (return a) n) a n :=
id                                           └─────┘  └────┘  └────┘      
src                                           └─────┘  └────┘  └────┘
typ                                          └─────┘  └────┘  └────┘      
doc                                           └─────┘  └────┘  └────┘
424  by have := results_thinkN n (results_ret a); rwa zero_add at this
id              └────────────┘   └─────────┘        └──────┘
src     └──────┘└────────────┘  └─────────┘   └──┘└──────┘└────────
typ     └──────┘└────────────┘ └─────────┘  └──┘└──────┘└────────
doc     └──────┘                              └──┘        └────────
txt     └──────┘                              └──┘        └────────
par     └──────┘                              └──┘        └────────
pid     └───┘└─┘                                         └──────┘
st     └─────────────────────────────────────────────┘└──────┘└────────
425  
src  
typ  
doc  
txt  
par  
pid  
st   
426  @[simp] theorem length_thinkN (s : computation α) [h : terminates s] (n) :
id                                      └─────────┘        └────────┘ 
src                                     └─────────┘         └────────┘
typ                                     └─────────┘        └────────┘ 
doc    └──┘                             └─────────┘         └────────┘
427    length (thinkN s n) = length s + n :=
id     └────┘  └────┘     └────┘   
src    └────┘  └────┘       └────┘   
typ    └────┘  └────┘     └────┘   
doc    └────┘  └────┘        └────┘
428  (results_thinkN n (results_of_terminates _)).length
id    └────────────┘   └───────────────────┘    └────┘
src   └────────────┘    └───────────────────┘    └────┘
typ   └────────────┘   └───────────────────┘    └────┘
429  
430  theorem eq_thinkN {s : computation α} {a n} (h : results s a n) :
id                          └─────────┘              └─────┘   
src                         └─────────┘               └─────┘
typ                         └─────────┘              └─────┘   
doc                         └─────────┘               └─────┘
431    s = thinkN (return a) n :=
id       └────┘  └────┘   
src       └────┘  └────┘
typ      └────┘  └────┘   
doc        └────┘  └────┘
432  begin
st   └─────
433    revert s,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          └┘
st   ─────────┘└─
434    induction n with n IH; intro s;
id               
src    └────────┘ └────────┘  └─────┘
typ    └────────┘└────────┘  └─────┘
doc    └────────┘ └────────┘  └─────┘
txt    └────────┘ └────────┘  └─────┘
par    └────────┘ └────────┘  └─────┘
pid              └───────┘       └┘
st   ──────────────────────────────────
435    apply cases_on s (λ a', _) (λ s, _); intro h,
id           └──────┘ 
src    └────┘└──────┘   └──────┘  └────┘  └─────┘
typ    └────┘└──────┘  └──────┘  └────┘  └─────┘
doc    └────┘           └──────┘  └────┘  └─────┘
txt    └────┘           └──────┘  └────┘  └─────┘
par    └────┘           └──────┘  └────┘  └─────┘
pid                    └──────┘  └────┘       └┘
st   ─────────────────────────────────────────────┘└─
436    { rw ←eq_of_ret_mem h.mem, refl },
id           └───────────┘ └───┘
src      └──┘└───────────┘└───┘  └───┘
typ      └──┘└───────────┘└───┘  └───┘
doc      └──┘                    └───┘
txt      └──┘                    └───┘
par      └──┘                    └───┘
pid        └┘                        
st   ───┘└─────────────────────┘└─────┘└┘
437    { cases of_results_think h with n h, cases h, contradiction },
id             └──────────────┘                  
src      └────┘└──────────────┘ └───────┘  └────┘   └────────────┘
typ      └────┘└──────────────┘└───────┘  └────┘  └────────────┘
doc      └────┘                 └───────┘  └────┘   └────────────┘
txt      └────┘                 └───────┘  └────┘   └────────────┘
par      └────┘                 └───────┘  └────┘   └────────────┘
pid                            └───────┘                       
st   ───┘└───────────────────────────────┘└───────┘└──────────────┘└┘
438    { have := h.len_unique (results_ret _), contradiction },
id               └──────────┘  └─────────┘
src      └──────┘└──────────┘ └─────────┘└─┘  └────────────┘
typ      └──────┘└──────────┘ └─────────┘└─┘  └────────────┘
doc      └──────┘                        └─┘  └────────────┘
txt      └──────┘                        └─┘  └────────────┘
par      └──────┘                        └─┘  └────────────┘
pid      └───┘└─┘                        └─┘               
st   ───┘└──────────────────────────────────┘└──────────────┘└┘
439    { rw IH (results_think_iff.1 h), refl }
id          └┘  └───────────────┘   
src      └─┘   └───────────────┘└─┘   └───┘
typ      └─┘└┘ └───────────────┘└─┘  └───┘
doc      └─┘                    └─┘   └───┘
txt      └─┘                    └─┘   └───┘
par      └─┘                    └─┘   └───┘
pid                            └─┘       
st   ────────────────────────────────┘└─────┘└─
440  end
st   ──┘
441  
442  theorem eq_thinkN' (s : computation α) [h : terminates s] :
id                           └─────────┘        └────────┘ 
src                          └─────────┘         └────────┘
typ                          └─────────┘        └────────┘ 
doc                          └─────────┘         └────────┘
443    s = thinkN (return (get s)) (length s) :=
id       └────┘  └────┘  └─┘     └────┘ 
src       └────┘  └────┘  └─┘      └────┘
typ      └────┘  └────┘  └─┘     └────┘ 
doc        └────┘  └────┘  └─┘      └────┘
444  eq_thinkN (results_of_terminates _)
id   └───────┘  └───────────────────┘
src  └───────┘  └───────────────────┘
typ  └───────┘  └───────────────────┘
445  
446  def mem_rec_on {C : computation α → Sort v} {a s} (M : a ∈ s)
id                       └─────────┘                         
src                      └─────────┘                          
typ                      └─────────┘                         
doc                      └─────────┘
447    (h1 : C (return a)) (h2 : ∀ s, C s → C (think s)) : C s :=
id             └────┘                    └───┘       
src             └────┘                         └───┘
typ            └────┘                    └───┘       
doc             └────┘                         └───┘
448  begin
st   └─────
449    haveI T := terminates_of_mem M,
id                └───────────────┘ 
src    └─────────┘└───────────────┘
typ    └─────────┘└───────────────┘
doc    └─────────┘                 
txt    └─────────┘                 
par    └─────────┘                 
pid         └┘└─┘                 
st   ───────────────────────────────┘└─
450    rw [eq_thinkN' s, get_eq_of_mem s M],
id         └────────┘   └───────────┘  
src    └──┘└────────┘ └┘└───────────┘  
typ    └──┘└────────┘└┘└───────────┘
doc    └──┘           └┘               
txt    └──┘           └┘               
par    └──┘           └┘               
pid      └┘           └┘               
st   ─────────────────┘└─────────────────┘└──
451    generalize : length s = n,
id                  └────┘ 
src    └───────────┘└────┘  
typ    └───────────┘└────┘ 
doc    └───────────┘└────┘  
txt    └───────────┘        
par    └───────────┘        
pid                      
st   ──────────────────────────┘└─
452    induction n with n IH, exacts [h1, h2 _ IH]
id                                   └┘  └┘   └┘
src    └────────┘ └────────┘  └──────┘  └┘  └─┘  └┘
typ    └────────┘└────────┘  └──────┘└┘└┘└┘└─┘└┘└┘
doc    └────────┘ └────────┘  └──────┘  └┘  └─┘  └┘
txt    └────────┘ └────────┘  └──────┘  └┘  └─┘  └┘
par    └────────┘ └────────┘  └──────┘  └┘  └─┘  └┘
pid              └───────┘        └┘  └┘  └─┘  
st   ──────────────────────┘└─────────────────────┘
453  end
st   └─┘
454  
455  def terminates_rec_on {C : computation α → Sort v} (s) [terminates s]
id                              └─────────┘                 └────────┘ 
src                             └─────────┘                  └────────┘
typ                             └─────────┘                 └────────┘ 
doc                             └─────────┘                  └────────┘
456    (h1 : ∀ a, C (return a)) (h2 : ∀ s, C s → C (think s)) : C s :=
id                 └────┘                    └───┘       
src                  └────┘                         └───┘
typ                └────┘                    └───┘       
doc                  └────┘                         └───┘
457  mem_rec_on (get_mem s) (h1 _) h2
id   └────────┘  └─────┘    └┘    └┘
src  └────────┘  └─────┘
typ  └────────┘  └─────┘    └┘    └┘
458  
459  /-- Map a function on the result of a computation. -/
460  def map (f : α → β) : computation α → computation β
id                       └─────────┘   └─────────┘ 
src                        └─────────┘     └─────────┘
typ                      └─────────┘   └─────────┘ 
doc                        └─────────┘     └─────────┘
461  | ⟨s, al⟩ := ⟨s.map (λo, option.cases_on o none (some ∘ f)),
id                 └──┘     └─────────────┘  └──┘  └──┘  
src                 └──┘      └─────────────┘   └──┘  └──┘ 
typ                └──┘     └─────────────┘  └──┘  └──┘  
462  λn b, begin
id     
typ    
st         └─────
463    dsimp [stream.map, stream.nth],
id            └────────┘  └────────┘
src    └─────┘└────────┘└┘└────────┘
typ    └─────┘└────────┘└┘└────────┘
doc    └─────┘          └┘          
txt    └─────┘          └┘          
par    └─────┘          └┘          
pid                   └┘          
st   ───────────────────────────────┘└─
464    induction e : s n with a; intro h,
id                    
src    └────────┘ └─┘  └─────┘  └─────┘
typ    └────────┘ └─┘└─────┘  └─────┘
doc    └────────┘ └─┘  └─────┘  └─────┘
txt    └────────┘ └─┘  └─────┘  └─────┘
par    └────────┘ └─┘  └─────┘  └─────┘
pid              └─┘  └────┘       └┘
st   ──────────────────────────────────┘└─
465    { contradiction }, { rw [al e, ←h] }
id                              └┘    
src      └────────────┘     └──┘   └─┘ └┘
typ      └────────────┘     └──┘└┘└─┘└┘
doc      └────────────┘     └──┘   └─┘ └┘
txt      └────────────┘     └──┘   └─┘ └┘
par      └────────────┘     └──┘   └─┘ └┘
pid                          └┘   └─┘ 
st   ───┘└────────────┘└┘└─────────┘└──┘└─
466  end⟩
st   ──┘
467  
468  def bind.G : β ⊕ computation β → β ⊕ computation α ⊕ computation β
id                  └─────────┘     └─────────┘   └─────────┘ 
src                  └─────────┘        └─────────┘    └─────────┘
typ                 └─────────┘     └─────────┘   └─────────┘ 
doc                   └─────────┘         └─────────┘     └─────────┘
469  | (sum.inl b)   := sum.inl b
id      └─────┘        └─────┘
src     └─────┘         └─────┘
typ     └─────┘        └─────┘
470  | (sum.inr cb') := sum.inr $ sum.inr cb'
id      └─────┘ └─┘     └─────┘   └─────┘
src     └─────┘         └─────┘   └─────┘
typ     └─────┘ └─┘     └─────┘   └─────┘
471  
472  def bind.F (f : α → computation β) :
id                      └─────────┘ 
src                      └─────────┘
typ                     └─────────┘ 
doc                      └─────────┘
473    computation α ⊕ computation β → β ⊕ computation α ⊕ computation β
id     └─────────┘   └─────────┘     └─────────┘   └─────────┘ 
src    └─────────┘    └─────────┘        └─────────┘    └─────────┘
typ    └─────────┘   └─────────┘     └─────────┘   └─────────┘ 
doc    └─────────┘     └─────────┘         └─────────┘     └─────────┘
474  | (sum.inl ca) :=
id      └─────┘ └┘
src     └─────┘
typ     └─────┘ └┘
475    match destruct ca with
id           └──────┘
src          └──────┘
typ          └──────┘
doc          └──────┘
476    | sum.inl a := bind.G $ destruct (f a)
id       └─────┘     └────┘   └──────┘  
src      └─────┘      └────┘   └──────┘
typ      └─────┘     └────┘   └──────┘  
doc                            └──────┘
477    | sum.inr ca' := sum.inr $ sum.inl ca'
id       └─────┘ └─┘    └─────┘   └─────┘
src      └─────┘        └─────┘   └─────┘
typ      └─────┘ └─┘    └─────┘   └─────┘
478    end
479  | (sum.inr cb) := bind.G $ destruct cb
id      └─────┘ └┘     └────┘   └──────┘
src     └─────┘        └────┘   └──────┘
typ     └─────┘ └┘     └────┘   └──────┘
doc                             └──────┘
480  
481  /-- Compose two computations into a monadic `bind` operation. -/
482  def bind (c : computation α) (f : α → computation β) : computation β :=
id                 └─────────┘           └─────────┘     └─────────┘ 
src                └─────────┘             └─────────┘      └─────────┘
typ                └─────────┘           └─────────┘     └─────────┘ 
doc                └─────────┘             └─────────┘      └─────────┘
483  corec (bind.F f) (sum.inl c)
id   └───┘  └────┘    └─────┘ 
src  └───┘  └────┘     └─────┘
typ  └───┘  └────┘    └─────┘ 
doc  └───┘
484  
485  instance : has_bind computation := ⟨@bind⟩
id              └──────┘ └─────────┘      └──┘
src             └──────┘ └─────────┘      └──┘
typ             └──────┘ └─────────┘      └──┘
doc                      └─────────┘      └──┘
486  
487  theorem has_bind_eq_bind {β} (c : computation α) (f : α → computation β) :
id                                     └─────────┘           └─────────┘ 
src                                    └─────────┘             └─────────┘
typ                                    └─────────┘           └─────────┘ 
doc                                    └─────────┘             └─────────┘
488    c >>= f = bind c f := rfl
id      └─┘   └──┘      └─┘
src      └─┘    └──┘        └─┘
typ     └─┘   └──┘      └─┘
doc              └──┘
489  
490  /-- Flatten a computation of computations into a single computation. -/
491  def join (c : computation (computation α)) : computation α := c >>= id
id                 └─────────┘  └─────────┘      └─────────┘      └─┘ └┘
src                └─────────┘  └─────────┘       └─────────┘        └─┘ └┘
typ                └─────────┘  └─────────┘      └─────────┘      └─┘ └┘
doc                └─────────┘  └─────────┘       └─────────┘
492  
493  @[simp] theorem map_ret (f : α → β) (a) : map f (return a) = return (f a) := rfl
id                                           └─┘   └────┘    └────┘        └─┘
src                                            └─┘    └────┘     └────┘          └─┘
typ                                          └─┘   └────┘    └────┘        └─┘
doc    └──┘                                    └─┘    └────┘      └────┘
494  
495  @[simp] theorem map_think (f : α → β) : ∀ s, map f (think s) = think (map f s)
id                                             └─┘   └───┘    └───┘  └─┘  
src                                               └─┘    └───┘     └───┘  └─┘
typ                                            └─┘   └───┘    └───┘  └─┘  
doc    └──┘                                       └─┘    └───┘      └───┘  └─┘
496  | ⟨s, al⟩ := by apply subtype.eq; dsimp [think, map]; rw stream.map_cons
id                         └────────┘         └───┘  └─┘      └─────────────┘
src                  └────┘└────────┘  └─────┘└───┘└┘└─┘  └─┘└─────────────┘
typ                  └────┘└────────┘  └─────┘└───┘└┘└─┘  └─┘└─────────────┘
doc                  └────┘            └─────┘└───┘└┘└─┘  └─┘               
txt                  └────┘            └─────┘     └┘     └─┘               
par                  └────┘            └─────┘     └┘     └─┘               
pid                                             └┘                      
st                  └────────────────────────────────────────┘└─────────────┘
497  
src  
typ  
doc  
txt  
par  
pid  
st   
498  @[simp] theorem destruct_map (f : α → β) (s) : destruct (map f s) = lmap f (rmap (map f) (destruct s)) :=
id                                                └──────┘  └─┘     └──┘   └──┘  └─┘    └──────┘ 
src                                                 └──────┘  └─┘       └──┘    └──┘  └─┘     └──────┘
typ                                               └──────┘  └─┘     └──┘   └──┘  └─┘    └──────┘ 
doc    └──┘                                         └──────┘  └─┘        └──┘    └──┘  └─┘     └──────┘
499  by apply s.cases_on; intro; simp
src     └────┘            └───┘  └────
typ     └────┘            └───┘  └────
doc     └────┘            └───┘  └────
txt     └────┘            └───┘  └────
par     └────┘            └───┘  └────
pid                                 
st     └──────────────────────────────
500  
src  
typ  
doc  
txt  
par  
pid  
st   
501  @[simp] theorem map_id : ∀ (s : computation α), map id s = s
id                                  └─────────┘    └─┘ └┘   
src                                  └─────────┘     └─┘ └┘   
typ                                 └─────────┘    └─┘ └┘   
doc    └──┘                          └─────────┘     └─┘
502  | ⟨f, al⟩ := begin
st                └─────
503    apply subtype.eq; simp [map, function.comp],
id           └────────┘        └─┘  └───────────┘
src    └────┘└────────┘  └────┘└─┘└┘└───────────┘
typ    └────┘└────────┘  └────┘└─┘└┘└───────────┘
doc    └────┘            └────┘└─┘└┘             
txt    └────┘            └────┘   └┘             
par    └────┘            └────┘   └┘             
pid                            └┘             
st   ────────────────────────────────────────────┘└─
504    have e : (@option.rec α (λ_, option α) none some) = id,
id                └────────┘        └────┘   └──┘ └──┘   └┘
src    └───────┘  └────────┘   └─┘└────┘ └┘└──┘└──┘└┘└┘
typ    └───────┘  └────────┘   └─┘└────┘└┘└──┘└──┘└┘└┘
doc    └───────┘               └─┘       └┘        └┘ 
txt    └───────┘               └─┘       └┘        └┘ 
par    └───────┘               └─┘       └┘        └┘ 
pid    └────┘└─┘               └─┘       └┘        └┘ 
st   ───────────────────────────────────────────────────────┘└─
505    { funext x, cases x; refl },
id                       
src      └──────┘  └────┘   └───┘
typ      └──────┘  └────┘  └───┘
doc      └──────┘  └────┘   └───┘
txt      └──────┘  └────┘   └───┘
par      └──────┘  └────┘   └───┘
pid            └┘              
st   ───┘└──────┘└──────────────┘└┘
506    simp [e, stream.map_id]
id             └───────────┘
src    └────┘ └┘└───────────┘└┘
typ    └────┘└┘└───────────┘└┘
doc    └────┘ └┘             └┘
txt    └────┘ └┘             └┘
par    └────┘ └┘             └┘
pid         └┘             
st   ─────────────────────────┘
507  end
st   └─┘
508  
509  theorem map_comp (f : α → β) (g : β → γ) :
id                                      
typ                                     
510    ∀ (s : computation α), map (g ∘ f) s = map g (map f s)
id           └─────────┘    └─┘        └─┘   └─┘  
src           └─────────┘     └─┘           └─┘    └─┘
typ          └─────────┘    └─┘        └─┘   └─┘  
doc           └─────────┘     └─┘             └─┘    └─┘
511  | ⟨s, al⟩ := begin
st                └─────
512    apply subtype.eq; dsimp [map],
id           └────────┘         └─┘
src    └────┘└────────┘  └─────┘└─┘
typ    └────┘└────────┘  └─────┘└─┘
doc    └────┘            └─────┘└─┘
txt    └────┘            └─────┘   
par    └────┘            └─────┘   
pid                             
st   ──────────────────────────────┘└─
513    rw stream.map_map,
id        └────────────┘
src    └─┘└────────────┘
typ    └─┘└────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────┘└─
514    apply congr_arg (λ f : _ → option γ, stream.map f s),
id           └───────┘           └────┘   └────────┘   
src    └────┘└───────┘  └─────┘ └────┘ └┘└────────┘  
typ    └────┘└───────┘  └─────┘└────┘└┘└────────┘ 
doc    └────┘           └─────┘        └┘            
txt    └────┘           └─────┘        └┘            
par    └────┘           └─────┘        └┘            
pid                    └─────┘        └┘            
st   ─────────────────────────────────────────────────────┘└─
515    funext x, cases x with x; refl
id                     
src    └──────┘  └────┘ └─────┘  └───┘
typ    └──────┘  └────┘└─────┘  └───┘
doc    └──────┘  └────┘ └─────┘  └───┘
txt    └──────┘  └────┘ └─────┘  └───┘
par    └──────┘  └────┘ └─────┘  └───┘
pid          └┘        └─────┘      
st   ─────────┘└─────────────────────┘
516  end
st   └─┘
517  
518  @[simp] theorem ret_bind (a) (f : α → computation β) :
id                                        └─────────┘ 
src                                        └─────────┘
typ                                       └─────────┘ 
doc    └──┘                                └─────────┘
519    bind (return a) f = f a :=
id     └──┘  └────┘      
src    └──┘  └────┘      
typ    └──┘  └────┘      
doc    └──┘  └────┘
520  begin
st   └─────
521    apply eq_of_bisim (λc₁ c₂,
id           └─────────┘
src    └────┘└─────────┘  └──────
typ    └────┘└─────────┘  └──────
doc    └────┘             └──────
txt    └────┘             └──────
par    └────┘             └──────
pid                      └──────
st   ─────────────────────────────
522           c₁ = bind (return a) f ∧ c₂ = f a ∨
id                └──┘  └────┘               
src  ────────┘  └──┘ └────┘ └┘      
typ  ────────┘  └──┘ └────┘ └┘     
doc  ────────┘   └──┘ └────┘ └┘        
txt  ────────┘               └┘        
par  ────────┘               └┘        
pid  ────────┘               └┘        
st   ─────────────────────────────────────────────
523           c₁ = corec (bind.F f) (sum.inr c₂)),
id                 └───┘  └────┘    └─────┘
src  ────────┘   └───┘ └────┘ └┘ └─────┘  └┘
typ  ────────┘   └───┘ └────┘└┘ └─────┘  └┘
doc  ────────┘   └───┘        └┘          └┘
txt  ────────┘                └┘          └┘
par  ────────┘                └┘          └┘
pid  ────────┘                └┘          └┘
st   ───────────────────────────────────────────┘└─
524    { intros c₁ c₂ h,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ───┘└────────────┘└─
525      exact match c₁, c₂, h with
id                   └┘  └┘  
src      └────┘       └┘  └┘ └─────
typ      └────┘     └┘└┘└┘└┘└─────
doc      └────┘       └┘  └┘ └─────
txt      └────┘       └┘  └┘ └─────
par      └────┘       └┘  └┘ └─────
pid                  └┘  └┘ └─────
st   ───────────────────────────────
526      | ._, ._, or.inl ⟨rfl, rfl⟩ := begin
id                 └────┘       └─┘
src  ─────┘  └┘  └┘└────┘    └┘└─┘└───┘     
typ  ─────┘  └┘  └┘└────┘    └┘└─┘└───┘     
doc  ─────┘  └┘  └┘          └┘   └───┘     
txt  ─────┘  └┘  └┘          └┘   └───┘     
par  ─────┘  └┘  └┘          └┘   └───┘     
pid  ─────┘  └┘  └┘          └┘   └───┘     
st   ──────────────────────────────────┘└─────
527        simp [bind, bind.F],
id               └──┘  └────┘
src  ─────┘└────┘└──┘└┘└────┘└─
typ  ─────┘└────┘└──┘└┘└────┘└─
doc  ─────┘└────┘└──┘└┘      └─
txt  ─────┘└────┘    └┘      └─
par  ─────┘└────┘    └┘      └─
pid  ───────────┘    └┘      └──
st   ────────────────────────┘└─
528        cases destruct (f a) with b cb; simp [bind.G]
id               └──────┘                      └────┘
src  ─────┘└────┘└──────┘   └─────────┘└┘└────┘└────┘└─
typ  ─────┘└────┘└──────┘ └─────────┘└┘└────┘└────┘└─
doc  ─────┘└────┘└──────┘   └─────────┘└┘└────┘      └─
txt  ─────┘└────┘           └─────────┘└┘└────┘      └─
par  ─────┘└────┘           └─────────┘└┘└────┘      └─
pid  ───────────┘           └─────────────────┘      └─
st   ────────────────────────────────────────────────────
529      end
src  ───┘└───
typ  ───┘└───
doc  ───┘└───
txt  ───┘└───
par  ───┘└───
pid  ────────
st   ───┘└─┘
530      | ._, c, or.inr rfl := begin
id                └────┘
src  ─────┘  └┘ └┘└────┘   └──┘     
typ  ─────┘  └┘ └┘└────┘   └──┘     
doc  ─────┘  └┘ └┘         └──┘     
txt  ─────┘  └┘ └┘         └──┘     
par  ─────┘  └┘ └┘         └──┘     
pid  ─────┘  └┘ └┘         └──┘     
st   ──────────────────────────┘└─────
531        simp [bind.F],
id               └────┘
src  ─────┘└────┘└────┘└─
typ  ─────┘└────┘└────┘└─
doc  ─────┘└────┘      └─
txt  ─────┘└────┘      └─
par  ─────┘└────┘      └─
pid  ───────────┘      └──
st   ──────────────────┘└─
532        cases destruct c with b cb; simp [bind.G]
id               └──────┘                   └────┘
src  ─────┘└────┘└──────┘ └────────┘└┘└────┘└────┘└─
typ  ─────┘└────┘└──────┘└────────┘└┘└────┘└────┘└─
doc  ─────┘└────┘└──────┘ └────────┘└┘└────┘      └─
txt  ─────┘└────┘         └────────┘└┘└────┘      └─
par  ─────┘└────┘         └────────┘└┘└────┘      └─
pid  ───────────┘         └────────────────┘      └─
st   ────────────────────────────────────────────────
533      end end },
src  ───┘└──────┘
typ  ───┘└──────┘
doc  ───┘└──────┘
txt  ───┘└──────┘
par  ───┘└──────┘
pid  ──────────┘
st   ───┘└─┘└───┘└┘
534    { simp }
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└─
535  end
st   ──┘
536  
537  @[simp] theorem think_bind (c) (f : α → computation β) :
id                                          └─────────┘ 
src                                          └─────────┘
typ                                         └─────────┘ 
doc    └──┘                                  └─────────┘
538    bind (think c) f = think (bind c f) :=
id     └──┘  └───┘     └───┘  └──┘  
src    └──┘  └───┘       └───┘  └──┘
typ    └──┘  └───┘     └───┘  └──┘  
doc    └──┘  └───┘        └───┘  └──┘
539  destruct_eq_think $ by simp [bind, bind.F]
id   └───────────────┘            └──┘  └────┘
src  └───────────────┘      └────┘└──┘└┘└────┘└─
typ  └───────────────┘      └────┘└──┘└┘└────┘└─
doc                         └────┘└──┘└┘      └─
txt                         └────┘    └┘      └─
par                         └────┘    └┘      └─
pid                                 └┘      
st                         └────────────────────
540  
src  
typ  
doc  
txt  
par  
pid  
st   
541  @[simp] theorem bind_ret (f : α → β) (s) : bind s (return ∘ f) = map f s :=
id                                            └──┘   └────┘     └─┘  
src                                             └──┘    └────┘      └─┘
typ                                           └──┘   └────┘     └─┘  
doc    └──┘                                     └──┘    └────┘        └─┘
542  begin
st   └─────
543    apply eq_of_bisim (λc₁ c₂, c₁ = c₂ ∨
id           └─────────┘                 
src    └────┘└─────────┘  └─────┘    
typ    └────┘└─────────┘  └─────┘    
doc    └────┘             └─────┘      
txt    └────┘             └─────┘      
par    └────┘             └─────┘      
pid                      └─────┘      
st   ───────────────────────────────────────
544           ∃ s, c₁ = bind s (return ∘ f) ∧ c₂ = map f s),
id                    └──┘    └────┘           └─┘ 
src  ────────┘└┘   └──┘  └────┘ └┘   └─┘  
typ  ────────┘└┘   └──┘  └────┘ └┘   └─┘ 
doc  ────────┘ └┘    └──┘  └────┘  └┘    └─┘  
txt  ────────┘ └┘                  └┘         
par  ────────┘ └┘                  └┘         
pid  ────────┘ └┘                  └┘         
st   ─────────────────────────────────────────────────────┘└─
545    { intros c₁ c₂ h,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ───┘└────────────┘└─
546      exact match c₁, c₂, h with
id                   └┘  └┘  
src      └────┘       └┘  └┘ └─────
typ      └────┘     └┘└┘└┘└┘└─────
doc      └────┘       └┘  └┘ └─────
txt      └────┘       └┘  └┘ └─────
par      └────┘       └┘  └┘ └─────
pid                  └┘  └┘ └─────
st   ───────────────────────────────
547      | _, _, or.inl (eq.refl c) := begin cases destruct c with b cb; simp end
id               └────┘  └─────┘                   └──────┘ 
src  ───────────┘└────┘ └─────┘ └───┘     └────┘└──────┘ └────────┘└┘└───┘└───
typ  ───────────┘└────┘ └─────┘ └───┘     └────┘└──────┘└────────┘└┘└───┘└───
doc  ───────────┘               └───┘     └────┘└──────┘ └────────┘└┘└───┘└───
txt  ───────────┘               └───┘     └────┘         └────────┘└┘└───┘└───
par  ───────────┘               └───┘     └────┘         └────────┘└┘└───┘└───
pid  ───────────┘               └───┘     └─────┘         └────────────────────
st   ─────────────────────────────────┘└─────────────────────────────────────┘└─┘
548      | _, _, or.inr ⟨s, rfl, rfl⟩ := begin
id               └────┘          └─┘
src  ───────────┘└────┘  └┘   └┘└─┘└───┘     
typ  ───────────┘└────┘  └┘   └┘└─┘└───┘     
doc  ───────────┘        └┘   └┘   └───┘     
txt  ───────────┘        └┘   └┘   └───┘     
par  ───────────┘        └┘   └┘   └───┘     
pid  ───────────┘        └┘   └┘   └───┘     
st   ───────────────────────────────────┘└─────
549        apply cases_on s; intros s; simp,
id               └──────┘ 
src  ─────┘└────┘└──────┘ └┘└──────┘└┘└──┘└─
typ  ───────────┘└──────┘└┘└──────┘└┘└──┘└─
doc  ─────┘└────┘         └┘└──────┘└┘└──┘└─
txt  ─────┘└────┘         └┘└──────┘└┘└──┘└─
par  ───────────┘         └┘└──────┘└┘└──┘└─
pid  ───────────┘         └─────────────────
st   ─────────────────────────────────────┘└─
550        exact or.inr ⟨s, rfl, rfl⟩
id               └────┘         └─┘
src  ───────────┘└────┘  └┘   └┘└─┘└─
typ  ───────────┘└────┘ └┘   └┘└─┘└─
doc  ───────────┘        └┘   └┘   └─
txt  ───────────┘        └┘   └┘   └─
par  ───────────┘        └┘   └┘   └─
pid  ───────────┘        └┘   └┘   └─
st   ─────────────────────────────────
551      end end },
src  ───────────┘
typ  ───────────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ──────────┘
st   ───┘└─┘└───┘└┘
552    { exact or.inr ⟨s, rfl, rfl⟩ }
id             └────┘         └─┘
src      └────┘└────┘  └┘   └┘└─┘└┘
typ      └────┘└────┘ └┘   └┘└─┘└┘
doc      └────┘        └┘   └┘   └┘
txt      └────┘        └┘   └┘   └┘
par      └────┘        └┘   └┘   └┘
pid                   └┘   └┘   
st   ──────────────────────────────┘└─
553  end
st   ──┘
554  
555  @[simp] theorem bind_ret' (s : computation α) : bind s return = s :=
id                                  └─────────┘     └──┘  └────┘  
src                                 └─────────┘      └──┘   └────┘ 
typ                                 └─────────┘     └──┘  └────┘  
doc    └──┘                         └─────────┘      └──┘   └────┘
556  by rw bind_ret; change (λ x : α, x) with @id α; rw map_id
id         └──────┘                           └┘      └────┘
src     └─┘└──────┘  └─────┘  └───┘ └┘ └─────┘ └┘   └─┘└────┘
typ     └─┘└──────┘  └─────┘  └───┘└┘ └─────┘ └┘  └─┘└────┘
doc     └─┘          └─────┘  └───┘ └┘ └─────┘      └─┘      
txt     └─┘          └─────┘  └───┘ └┘ └─────┘      └─┘      
par     └─┘          └─────┘  └───┘ └┘ └─────┘      └─┘      
pid                         └───┘ └┘ └────┘              
st     └───────────────────────────────────────────────┘└────┘
557  
src  
typ  
doc  
txt  
par  
pid  
st   
558  @[simp] theorem bind_assoc (s : computation α) (f : α → computation β) (g : β → computation γ) :
id                                   └─────────┘           └─────────┘           └─────────┘ 
src                                  └─────────┘             └─────────┘             └─────────┘
typ                                  └─────────┘           └─────────┘           └─────────┘ 
doc    └──┘                          └─────────┘             └─────────┘             └─────────┘
559    bind (bind s f) g = bind s (λ (x : α), bind (f x) g) :=
id     └──┘  └──┘      └──┘             └──┘     
src    └──┘  └──┘         └──┘               └──┘
typ    └──┘  └──┘      └──┘             └──┘     
doc    └──┘  └──┘          └──┘               └──┘
560  begin
st   └─────
561    apply eq_of_bisim (λc₁ c₂, c₁ = c₂ ∨
id           └─────────┘                 
src    └────┘└─────────┘  └─────┘    
typ    └────┘└─────────┘  └─────┘    
doc    └────┘             └─────┘      
txt    └────┘             └─────┘      
par    └────┘             └─────┘      
pid                      └─────┘      
st   ───────────────────────────────────────
562           ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s (λ (x : α), bind (f x) g)),
id                                                              └──┘      
src  ────────┘└┘              └┘           └────┘ └─┘└──┘   └┘ └┘
typ  ────────┘└┘              └┘           └────┘└─┘└──┘  └┘└┘
doc  ────────┘ └┘               └┘            └────┘ └─┘└──┘   └┘ └┘
txt  ────────┘ └┘               └┘            └────┘ └─┘       └┘ └┘
par  ────────┘ └┘               └┘            └────┘ └─┘       └┘ └┘
pid  ────────┘ └┘               └┘            └────┘ └─┘       └┘ └┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
563    { intros c₁ c₂ h,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ───┘└────────────┘└─
564      exact match c₁, c₂, h with
id                   └┘  └┘  
src      └────┘       └┘  └┘ └─────
typ      └────┘     └┘└┘└┘└┘└─────
doc      └────┘       └┘  └┘ └─────
txt      └────┘       └┘  └┘ └─────
par      └────┘       └┘  └┘ └─────
pid                  └┘  └┘ └─────
st   ───────────────────────────────
565      | _, _, or.inl (eq.refl c) := by cases destruct c with b cb; simp
id               └────┘  └─────┘                └──────┘ 
src  ───────────┘└────┘ └─────┘ └───┘  └────┘└──────┘ └────────┘└┘└────
typ  ───────────┘└────┘ └─────┘ └───┘  └────┘└──────┘└────────┘└┘└────
doc  ───────────┘               └───┘  └────┘└──────┘ └────────┘└┘└────
txt  ───────────┘               └───┘  └────┘         └────────┘└┘└────
par  ───────────┘               └───┘  └────┘         └────────┘└┘└────
pid  ───────────┘               └───┘  └─────┘         └────────────────
st   ───────────────────────────────────┘└─────────────────────────────────
566      | ._, ._, or.inr ⟨s, rfl, rfl⟩ := begin
id                 └────┘          └─┘
src  ───┘└┘  └┘  └┘└────┘  └┘   └┘└─┘└───┘     
typ  ───┘└┘  └┘  └┘└────┘  └┘   └┘└─┘└───┘     
doc  ───┘└┘  └┘  └┘        └┘   └┘   └───┘     
txt  ───┘└┘  └┘  └┘        └┘   └┘   └───┘     
par  ───┘└┘  └┘  └┘        └┘   └┘   └───┘     
pid  ─────┘  └┘  └┘        └┘   └┘   └───┘     
st   ───┘└────────────────────────────────┘└─────
567        apply cases_on s; intros s; simp,
id               └──────┘ 
src  ─────┘└────┘└──────┘ └┘└──────┘└┘└──┘└─
typ  ───────────┘└──────┘└┘└──────┘└┘└──┘└─
doc  ─────┘└────┘         └┘└──────┘└┘└──┘└─
txt  ─────┘└────┘         └┘└──────┘└┘└──┘└─
par  ───────────┘         └┘└──────┘└┘└──┘└─
pid  ───────────┘         └─────────────────
st   ─────────────────────────────────────┘└─
568        { generalize : f s = fs,
id                         
src  ───────┘└───────────┘     └─
typ  ───────┘└───────────┘   └─
doc  ───────┘└───────────┘     └─
txt  ───────┘└───────────┘     └─
par  ───────┘└───────────┘     └─
pid  ────────────────────┘     └─
st   ──────┘└────────────────────┘└─
569          apply cases_on fs; intros t; simp,
id                 └──────┘ └┘
src  ───────┘└────┘└──────┘  └┘└──────┘└┘└──┘└─
typ  ─────────────┘└──────┘└┘└┘└──────┘└┘└──┘└─
doc  ───────┘└────┘          └┘└──────┘└┘└──┘└─
txt  ───────┘└────┘          └┘└──────┘└┘└──┘└─
par  ─────────────┘          └┘└──────┘└┘└──┘└─
pid  ─────────────┘          └─────────────────
st   ────────────────────────────────────────┘└─
570          { cases destruct (g t) with b cb; simp } },
id                   └──────┘   
src  ─────────┘└────┘└──────┘   └─────────┘└┘└───┘└────
typ  ─────────┘└────┘└──────┘ └─────────┘└┘└───┘└────
doc  ─────────┘└────┘└──────┘   └─────────┘└┘└───┘└────
txt  ─────────┘└────┘           └─────────┘└┘└───┘└────
par  ─────────┘└────┘           └─────────┘└┘└───┘└────
pid  ───────────────┘           └──────────────────────
st   ──────────────────────────────────────────────┘└─┘└─
571        { exact or.inr ⟨s, rfl, rfl⟩ }
id                 └────┘         └─┘
src  ─────────────┘└────┘  └┘   └┘└─┘└───
typ  ─────────────┘└────┘ └┘   └┘└─┘└───
doc  ─────────────┘        └┘   └┘   └───
txt  ─────────────┘        └┘   └┘   └───
par  ─────────────┘        └┘   └┘   └───
pid  ─────────────┘        └┘   └┘   └───
st   ──────────────────────────────────┘└─
572      end end },
src  ───────────┘
typ  ───────────┘
doc  ───────────┘
txt  ───────────┘
par  ───────────┘
pid  ──────────┘
st   ──────┘└───┘└┘
573    { exact or.inr ⟨s, rfl, rfl⟩ }
id             └────┘         └─┘
src      └────┘└────┘  └┘   └┘└─┘└┘
typ      └────┘└────┘ └┘   └┘└─┘└┘
doc      └────┘        └┘   └┘   └┘
txt      └────┘        └┘   └┘   └┘
par      └────┘        └┘   └┘   └┘
pid                   └┘   └┘   
st   ──────────────────────────────┘└─
574  end
st   ──┘
575  
576  theorem results_bind {s : computation α} {f : α → computation β} {a b m n}
id                             └─────────┘           └─────────┘ 
src                            └─────────┘             └─────────┘
typ                            └─────────┘           └─────────┘ 
doc                            └─────────┘             └─────────┘
577    (h1 : results s a m) (h2 : results (f a) b n) : results (bind s f) b (n + m) :=
id           └─────┘           └─────┘          └─────┘  └──┘        
src          └─────┘              └─────┘              └─────┘  └──┘           
typ          └─────┘           └─────┘          └─────┘  └──┘        
doc          └─────┘              └─────┘              └─────┘  └──┘
578  begin
st   └─────
579    have := h1.mem, revert m,
id             └────┘
src    └──────┘└────┘  └──────┘
typ    └──────┘└────┘  └──────┘
doc    └──────┘        └──────┘
txt    └──────┘        └──────┘
par    └──────┘        └──────┘
pid    └───┘└─┘              └┘
st   ───────────────┘└────────┘└─
580    apply mem_rec_on this _ (λ s IH, _); intros m h1,
id           └────────┘ └──┘
src    └────┘└────────┘    └─┘  └───────┘  └─────────┘
typ    └────┘└────────┘└──┘└─┘  └───────┘  └─────────┘
doc    └────┘              └─┘  └───────┘  └─────────┘
txt    └────┘              └─┘  └───────┘  └─────────┘
par    └────┘              └─┘  └───────┘  └─────────┘
pid                       └─┘  └───────┘        └───┘
st   ─────────────────────────────────────────────────┘└─
581    { rw [ret_bind], rw h1.len_unique (results_ret _), exact h2 },
id           └──────┘      └───────────┘  └─────────┘           └┘
src      └──┘└──────┘  └─┘└───────────┘ └─────────┘└─┘  └────┘  
typ      └──┘└──────┘  └─┘└───────────┘ └─────────┘└─┘  └────┘└┘
doc      └──┘          └─┘                         └─┘  └────┘  
txt      └──┘          └─┘                         └─┘  └────┘  
par      └──┘          └─┘                         └─┘  └────┘  
pid        └┘                                     └─┘         
st   ───┘└──────────┘└─────────────────────────────────┘└─────────┘└┘
582    { rw [think_bind], cases of_results_think h1 with m' h, cases h with h1 e,
id           └────────┘         └──────────────┘ └┘                  
src      └──┘└────────┘  └────┘└──────────────┘  └────────┘  └────┘ └────────┘
typ      └──┘└────────┘  └────┘└──────────────┘└┘└────────┘  └────┘└────────┘
doc      └──┘            └────┘                  └────────┘  └────┘ └────────┘
txt      └──┘            └────┘                  └────────┘  └────┘ └────────┘
par      └──┘            └────┘                  └────────┘  └────┘ └────────┘
pid        └┘                                   └────────┘        └────────┘
st   ─────────────────┘└────────────────────────────────────┘└─────────────────┘└─
583      rw e, exact results_think (IH h1) }
id                  └───────────┘  └┘ └┘
src      └─┘   └────┘└───────────┘     └┘
typ      └─┘  └────┘└───────────┘ └┘└┘└┘
doc      └─┘   └────┘                  └┘
txt      └─┘   └────┘                  └┘
par      └─┘   └────┘                  └┘
pid                                  
st   ───────┘└────────────────────────────┘└─
584  end
st   ──┘
585  
586  theorem mem_bind {s : computation α} {f : α → computation β} {a b}
id                         └─────────┘           └─────────┘ 
src                        └─────────┘             └─────────┘
typ                        └─────────┘           └─────────┘ 
doc                        └─────────┘             └─────────┘
587    (h1 : a ∈ s) (h2 : b ∈ f a) : b ∈ bind s f :=
id                              └──┘  
src                                   └──┘
typ                             └──┘  
doc                                      └──┘
588  let ⟨m, h1⟩ := exists_results_of_mem h1,
id   └─┘     └┘     └───────────────────┘ └┘
src                 └───────────────────┘
typ  └─┘     └┘     └───────────────────┘ └┘
589      ⟨n, h2⟩ := exists_results_of_mem h2 in (results_bind h1 h2).mem
id           └┘     └───────────────────┘ └┘     └──────────┘       └─┘
src                 └───────────────────┘        └──────────┘       └─┘
typ          └┘     └───────────────────┘ └┘     └──────────┘       └─┘
590  
591  instance terminates_bind (s : computation α) (f : α → computation β)
id                                 └─────────┘           └─────────┘ 
src                                └─────────┘             └─────────┘
typ                                └─────────┘           └─────────┘ 
doc                                └─────────┘             └─────────┘
592    [terminates s] [terminates (f (get s))] :
id      └────────┘    └────────┘    └─┘ 
src     └────────┘     └────────┘     └─┘
typ     └────────┘    └────────┘    └─┘ 
doc     └────────┘     └────────┘     └─┘
593    terminates (bind s f) :=
id     └────────┘  └──┘  
src    └────────┘  └──┘
typ    └────────┘  └──┘  
doc    └────────┘  └──┘
594  terminates_of_mem (mem_bind (get_mem s) (get_mem (f (get s))))
id   └───────────────┘  └──────┘  └─────┘    └─────┘    └─┘ 
src  └───────────────┘  └──────┘  └─────┘     └─────┘     └─┘
typ  └───────────────┘  └──────┘  └─────┘    └─────┘    └─┘ 
doc                                                       └─┘
595  
596  @[simp] theorem get_bind (s : computation α) (f : α → computation β)
id                                 └─────────┘           └─────────┘ 
src                                └─────────┘             └─────────┘
typ                                └─────────┘           └─────────┘ 
doc    └──┘                        └─────────┘             └─────────┘
597    [terminates s] [terminates (f (get s))] :
id      └────────┘    └────────┘    └─┘ 
src     └────────┘     └────────┘     └─┘
typ     └────────┘    └────────┘    └─┘ 
doc     └────────┘     └────────┘     └─┘
598    get (bind s f) = get (f (get s)) :=
id     └─┘  └──┘     └─┘    └─┘ 
src    └─┘  └──┘       └─┘     └─┘
typ    └─┘  └──┘     └─┘    └─┘ 
doc    └─┘  └──┘        └─┘     └─┘
599  get_eq_of_mem _ (mem_bind (get_mem s) (get_mem (f (get s))))
id   └───────────┘    └──────┘  └─────┘    └─────┘    └─┘ 
src  └───────────┘    └──────┘  └─────┘     └─────┘     └─┘
typ  └───────────┘    └──────┘  └─────┘    └─────┘    └─┘ 
doc                                                     └─┘
600  
601  @[simp] theorem length_bind (s : computation α) (f : α → computation β)
id                                    └─────────┘           └─────────┘ 
src                                   └─────────┘             └─────────┘
typ                                   └─────────┘           └─────────┘ 
doc    └──┘                           └─────────┘             └─────────┘
602    [T1 : terminates s] [T2 : terminates (f (get s))] :
id           └────────┘         └────────┘    └─┘ 
src          └────────┘          └────────┘     └─┘
typ          └────────┘         └────────┘    └─┘ 
doc          └────────┘          └────────┘     └─┘
603    length (bind s f) = length (f (get s)) + length s :=
id     └────┘  └──┘     └────┘    └─┘     └────┘ 
src    └────┘  └──┘       └────┘     └─┘      └────┘
typ    └────┘  └──┘     └────┘    └─┘     └────┘ 
doc    └────┘  └──┘        └────┘     └─┘       └────┘
604  (results_of_terminates _).len_unique $
id    └───────────────────┘   └────────┘
src   └───────────────────┘   └────────┘
typ   └───────────────────┘   └────────┘
605  results_bind (results_of_terminates _) (results_of_terminates _)
id   └──────────┘  └───────────────────┘     └───────────────────┘
src  └──────────┘  └───────────────────┘     └───────────────────┘
typ  └──────────┘  └───────────────────┘     └───────────────────┘
606  
607  theorem of_results_bind {s : computation α} {f : α → computation β} {b k} :
id                                └─────────┘           └─────────┘ 
src                               └─────────┘             └─────────┘
typ                               └─────────┘           └─────────┘ 
doc                               └─────────┘             └─────────┘
608    results (bind s f) b k →
id     └─────┘  └──┘     
src    └─────┘  └──┘
typ    └─────┘  └──┘     
doc    └─────┘  └──┘
609    ∃ a m n, results s a m ∧ results (f a) b n ∧ k = n + m :=
id         └─────┘     └─────┘            
src           └─────┘        └─────┘                 
typ        └─────┘     └─────┘            
doc             └─────┘         └─────┘
610  begin
st   └─────
611    induction k with n IH generalizing s;
id               
src    └────────┘ └───────────────────────┘
typ    └────────┘└───────────────────────┘
doc    └────────┘ └───────────────────────┘
txt    └────────┘ └───────────────────────┘
par    └────────┘ └───────────────────────┘
pid              └───────┘└─────────────┘
st   ────────────────────────────────────────
612    apply cases_on s (λ a, _) (λ s', _); intro e,
id           └──────┘ 
src    └────┘└──────┘   └─────┘  └─────┘  └─────┘
typ    └────┘└──────┘  └─────┘  └─────┘  └─────┘
doc    └────┘           └─────┘  └─────┘  └─────┘
txt    └────┘           └─────┘  └─────┘  └─────┘
par    └────┘           └─────┘  └─────┘  └─────┘
pid                    └─────┘  └─────┘       └┘
st   ─────────────────────────────────────────────┘└─
613    { simp [thinkN] at e, refine ⟨a, _, _, results_ret _, e, rfl⟩ },
id             └────┘                        └─────────┘      └─┘
src      └────┘└────┘└────┘  └─────┘  └──────┘└─────────┘└──┘ └┘└─┘└┘
typ      └────┘└────┘└────┘  └─────┘ └──────┘└─────────┘└──┘└┘└─┘└┘
doc      └────┘└────┘└────┘  └─────┘  └──────┘           └──┘ └┘   └┘
txt      └────┘      └────┘  └─────┘  └──────┘           └──┘ └┘   └┘
par      └────┘      └────┘  └─────┘  └──────┘           └──┘ └┘   └┘
pid                └──┘          └──────┘           └──┘ └┘   
st   ───┘└────────────────┘└────────────────────────────────────────┘└┘
614    { have := congr_arg head (eq_thinkN e), contradiction },
id               └───────┘ └──┘  └───────┘ 
src      └──────┘└───────┘└──┘ └───────┘   └────────────┘
typ      └──────┘└───────┘└──┘ └───────┘  └────────────┘
doc      └──────┘         └──┘             └────────────┘
txt      └──────┘                          └────────────┘
par      └──────┘                          └────────────┘
pid      └───┘└─┘                                       
st   ───┘└──────────────────────────────────┘└──────────────┘└┘
615    { simp at e, refine ⟨a, _, n+1, results_ret _, e, rfl⟩ },
id                                  └─────────┘      └─┘
src      └───────┘  └─────┘  └───┘ └─┘└─────────┘└──┘ └┘└─┘└┘
typ      └───────┘  └─────┘ └───┘└─┘└─────────┘└──┘└┘└─┘└┘
doc      └───────┘  └─────┘  └───┘  └─┘           └──┘ └┘   └┘
txt      └───────┘  └─────┘  └───┘  └─┘           └──┘ └┘   └┘
par      └───────┘  └─────┘  └───┘  └─┘           └──┘ └┘   └┘
pid          └──┘          └───┘  └─┘           └──┘ └┘   
st   ───┘└───────┘└──────────────────────────────────────────┘└┘
616    { simp at e, exact let ⟨a, m, n', h1, h2, e'⟩ := IH e in
id                                                      └┘ 
src      └───────┘  └────┘     └┘ └┘  └┘  └┘  └┘  └───┘   └───
typ      └───────┘  └────┘     └┘ └┘  └┘  └┘  └┘  └───┘└┘└───
doc      └───────┘  └────┘     └┘ └┘  └┘  └┘  └┘  └───┘   └───
txt      └───────┘  └────┘     └┘ └┘  └┘  └┘  └┘  └───┘   └───
par      └───────┘  └────┘     └┘ └┘  └┘  └┘  └┘  └───┘   └───
pid          └──┘            └┘ └┘  └┘  └┘  └┘  └───┘   └───
st   ────────────┘└─────────────────────────────────────────────
617      by rw e'; exact ⟨a, m.succ, n', results_think h1, h2, rfl⟩ }
id             └┘           └────┘  └┘  └───────────┘ └┘  └┘  └─┘
src  ───┘  └─┘  └──────┘  └┘└────┘└┘  └┘└───────────┘  └┘  └┘└─┘└┘
typ  ───┘  └─┘└┘└──────┘ └┘└────┘└┘└┘└┘└───────────┘└┘└┘└┘└┘└─┘└┘
doc  ───┘  └─┘  └──────┘  └┘      └┘  └┘               └┘  └┘   └┘
txt  ───┘  └─┘  └──────┘  └┘      └┘  └┘               └┘  └┘   └┘
par  ───┘  └─┘  └──────┘  └┘      └┘  └┘               └┘  └┘   └┘
pid  ───┘  └──┘  └──────┘  └┘      └┘  └┘               └┘  └┘   └┘
st   ─────┘└───────────────────────────────────────────────────────┘└─
618  end
st   ──┘
619  
620  theorem exists_of_mem_bind {s : computation α} {f : α → computation β} {b}
id                                   └─────────┘           └─────────┘ 
src                                  └─────────┘             └─────────┘
typ                                  └─────────┘           └─────────┘ 
doc                                  └─────────┘             └─────────┘
621    (h : b ∈ bind s f) : ∃ a ∈ s, b ∈ f a :=
id            └──┘              
src            └──┘                 
typ           └──┘              
doc             └──┘
622  let ⟨k, h⟩ := exists_results_of_mem h,
id   └─┘          └───────────────────┘ 
src                └───────────────────┘
typ  └─┘          └───────────────────┘ 
623      ⟨a, m, n, h1, h2, e⟩ := of_results_bind h in ⟨a, h1.mem, h2.mem⟩
id                └┘  └┘        └─────────────┘            └──┘    └──┘
src                              └─────────────┘            └──┘    └──┘
typ               └┘  └┘        └─────────────┘            └──┘    └──┘
624  
625  theorem bind_promises {s : computation α} {f : α → computation β} {a b}
id                              └─────────┘           └─────────┘ 
src                             └─────────┘             └─────────┘
typ                             └─────────┘           └─────────┘ 
doc                             └─────────┘             └─────────┘
626    (h1 : s ~> a) (h2 : f a ~> b) : bind s f ~> b :=
id            └┘           └┘     └──┘   └┘ 
src            └┘              └┘      └──┘     └┘
typ           └┘           └┘     └──┘   └┘ 
doc            └┘              └┘      └──┘     └┘
627  λ b' bB, begin
id     └┘ └┘
typ    └┘ └┘
st            └─────
628    rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩,
id            └────────────────┘ └┘
src    └─────┘└────────────────┘  └──────────────────┘
typ    └─────┘└────────────────┘└┘└──────────────────┘
doc    └─────┘                    └──────────────────┘
txt    └─────┘                    └──────────────────┘
par    └─────┘                    └──────────────────┘
pid                              └──────────────────┘
st   ─────────────────────────────────────────────────┘└─
629    rw ←h1 a's at ba', exact h2 ba'
id         └┘ └─┘               └┘ └─┘
src    └──┘     └─────┘  └────┘     
typ    └──┘└┘└─┘└─────┘  └────┘└┘└─┘
doc    └──┘     └─────┘  └────┘     
txt    └──┘     └─────┘  └────┘     
par    └──┘     └─────┘  └────┘     
pid      └┘     └─────┘            
st   ──────────────────┘└─────────────┘
630  end
st   └─┘
631  
632  instance : monad computation :=
id              └───┘ └─────────┘
src             └───┘ └─────────┘
typ             └───┘ └─────────┘
doc                   └─────────┘
633  { map  := @map,
id              └─┘
src             └─┘
typ             └─┘
doc             └─┘
634    pure := @return,
id              └────┘
src             └────┘
typ             └────┘
doc             └────┘
635    bind := @bind }
id              └──┘
src             └──┘
typ             └──┘
doc             └──┘
636  
637  instance : is_lawful_monad computation :=
id              └─────────────┘ └─────────┘
src             └─────────────┘ └─────────┘
typ             └─────────────┘ └─────────┘
doc                             └─────────┘
638  { id_map := @map_id,
id               └────┘
src              └────┘
typ              └────┘
639    bind_pure_comp_eq_map := @bind_ret,
id                               └──────┘
src                              └──────┘
typ                              └──────┘
640    pure_bind := @ret_bind,
id                   └──────┘
src                  └──────┘
typ                  └──────┘
641    bind_assoc := @bind_assoc }
id                    └────────┘
src                   └────────┘
typ                   └────────┘
642  
643  theorem has_map_eq_map {β} (f : α → β) (c : computation α) : f <$> c = map f c := rfl
id                                             └─────────┘      └─┘   └─┘      └─┘
src                                              └─────────┘        └─┘    └─┘        └─┘
typ                                            └─────────┘      └─┘   └─┘      └─┘
doc                                              └─────────┘                └─┘
644  
645  @[simp] theorem return_def (a) : (_root_.return a : computation α) = return a := rfl
id                                     └───────────┘    └─────────┘    └────┘     └─┘
src                                    └───────────┘     └─────────┘     └────┘      └─┘
typ                                    └───────────┘    └─────────┘    └────┘     └─┘
doc    └──┘                                              └─────────┘      └────┘
646  
647  @[simp] theorem map_ret' {α β} : ∀ (f : α → β) (a), f <$> return a = return (f a) := map_ret
id                                                    └─┘ └────┘   └────┘        └─────┘
src                                                        └─┘ └────┘    └────┘          └─────┘
typ                                                   └─┘ └────┘   └────┘        └─────┘
doc    └──┘                                                    └────┘     └────┘
648  @[simp] theorem map_think' {α β} : ∀ (f : α → β) s, f <$> think s = think (f <$> s) := map_think
id                                                    └─┘ └───┘   └───┘   └─┘      └───────┘
src                                                        └─┘ └───┘    └───┘    └─┘       └───────┘
typ                                                   └─┘ └───┘   └───┘   └─┘      └───────┘
doc    └──┘                                                    └───┘     └───┘
649  
650  theorem mem_map (f : α → β) {a} {s : computation α} (m : a ∈ s) : f a ∈ map f s :=
id                                      └─────────┘                 └─┘  
src                                       └─────────┘                      └─┘
typ                                     └─────────┘                 └─┘  
doc                                       └─────────┘                        └─┘
651  by rw ←bind_ret; apply mem_bind m; apply ret_mem
id          └──────┘        └──────┘         └─────┘
src     └──┘└──────┘  └────┘└──────┘   └────┘└─────┘
typ     └──┘└──────┘  └────┘└──────┘  └────┘└─────┘
doc     └──┘          └────┘           └────┘       
txt     └──┘          └────┘           └────┘       
par     └──┘          └────┘           └────┘       
pid       └┘                                      
st     └──────────────────────────────────────────────
652  
src  
typ  
doc  
txt  
par  
pid  
st   
653  theorem exists_of_mem_map {f : α → β} {b : β} {s : computation α} (h : b ∈ map f s) :
id                                                   └─────────┘          └─┘  
src                                                     └─────────┘            └─┘
typ                                                  └─────────┘          └─┘  
doc                                                     └─────────┘             └─┘
654     ∃ a, a ∈ s ∧ f a = b :=
id               
src                  
typ              
655  by rw ←bind_ret at h; exact
id          └──────┘
src     └──┘└──────┘└───┘  └────┘
typ     └──┘└──────┘└───┘  └────┘
doc     └──┘        └───┘  └────┘
txt     └──┘        └───┘  └────┘
par     └──┘        └───┘  └────┘
pid       └┘        └───┘       
st     └─────────────────────────
656  let ⟨a, as, fb⟩ := exists_of_mem_bind h in ⟨a, as, mem_unique (ret_mem _) fb⟩
id          └┘  └┘     └────────────────┘             └────────┘  └─────┘
src       └┘  └┘  └───┘└────────────────┘ └──┘  └┘  └┘└────────┘ └─────┘└──┘  └─
typ      └┘└┘└┘└┘└───┘└────────────────┘└──┘  └┘  └┘└────────┘ └─────┘└──┘  └─
doc       └┘  └┘  └───┘                   └──┘  └┘  └┘                  └──┘  └─
txt       └┘  └┘  └───┘                   └──┘  └┘  └┘                  └──┘  └─
par       └┘  └┘  └───┘                   └──┘  └┘  └┘                  └──┘  └─
pid       └┘  └┘  └───┘                   └──┘  └┘  └┘                  └──┘  
st   ──────────────────────────────────────────────────────────────────────────────
657  
src  
typ  
doc  
txt  
par  
pid  
st   
658  instance terminates_map (f : α → β) (s : computation α) [terminates s] : terminates (map f s) :=
id                                          └─────────┘    └────────┘     └────────┘  └─┘  
src                                           └─────────┘     └────────┘      └────────┘  └─┘
typ                                         └─────────┘    └────────┘     └────────┘  └─┘  
doc                                           └─────────┘     └────────┘      └────────┘  └─┘
659  by rw ←bind_ret; apply_instance
id          └──────┘
src     └──┘└──────┘  └──────────────
typ     └──┘└──────┘  └──────────────
doc     └──┘          └──────────────
txt     └──┘          └──────────────
par     └──┘          └──────────────
pid       └┘                        
st     └─────────────────────────────
660  
src  
typ  
doc  
txt  
par  
pid  
st   
661  theorem terminates_map_iff (f : α → β) (s : computation α) :
id                                             └─────────┘ 
src                                              └─────────┘
typ                                            └─────────┘ 
doc                                              └─────────┘
662    terminates (map f s) ↔ terminates s :=
id     └────────┘  └─┘     └────────┘ 
src    └────────┘  └─┘       └────────┘
typ    └────────┘  └─┘     └────────┘ 
doc    └────────┘  └─┘        └────────┘
663  ⟨λ⟨a, h⟩, let ⟨b, h1, _⟩ := exists_of_mem_map h in ⟨_, h1⟩, @computation.terminates_map _ _ _ _⟩
id           └─┘     └┘        └───────────────┘                └────────────────────────┘
src                              └───────────────┘                └────────────────────────┘
typ          └─┘     └┘        └───────────────┘                └────────────────────────┘
664  
665  -- Parallel computation
666  /-- `c₁ <|> c₂` calculates `c₁` and `c₂` simultaneously, returning
667    the first one that gives a result. -/
668  def orelse (c₁ c₂ : computation α) : computation α :=
id                       └─────────┘     └─────────┘ 
src                      └─────────┘      └─────────┘
typ                      └─────────┘     └─────────┘ 
doc                      └─────────┘      └─────────┘
669  @computation.corec α (computation α × computation α)
id    └───────────────┘   └─────────┘   └─────────┘ 
src   └───────────────┘    └─────────┘    └─────────┘
typ   └───────────────┘   └─────────┘   └─────────┘ 
doc   └───────────────┘    └─────────┘     └─────────┘
670    (λ⟨c₁, c₂⟩, match destruct c₁ with
id       └┘  └┘         └──────┘
src                      └──────┘
typ      └┘  └┘         └──────┘
doc                      └──────┘
671    | sum.inl a := sum.inl a
id       └─────┘     └─────┘
src      └─────┘      └─────┘
typ      └─────┘     └─────┘
672    | sum.inr c₁' := match destruct c₂ with
id       └─────┘ └─┘          └──────┘
src      └─────┘              └──────┘
typ      └─────┘ └─┘          └──────┘
doc                           └──────┘
673      | sum.inl a := sum.inl a
id         └─────┘     └─────┘
src        └─────┘      └─────┘
typ        └─────┘     └─────┘
674      | sum.inr c₂' := sum.inr (c₁', c₂')
id         └─────┘ └─┘    └─────┘ 
src        └─────┘        └─────┘ 
typ        └─────┘ └─┘    └─────┘ 
675      end
676    end) (c₁, c₂)
id          └┘  └┘
src         
typ         └┘  └┘
677  
678  instance : alternative computation :=
id              └─────────┘ └─────────┘
src             └─────────┘ └─────────┘
typ             └─────────┘ └─────────┘
doc                         └─────────┘
679  { orelse := @orelse, failure := @empty, ..computation.monad }
id                └────┘              └───┘    └───────────────┘
src               └────┘              └───┘    └───────────────┘
typ               └────┘              └───┘    └───────────────┘
doc               └────┘              └───┘
680  
681  @[simp] theorem ret_orelse (a : α) (c₂ : computation α) :
id                                           └─────────┘ 
src                                           └─────────┘
typ                                          └─────────┘ 
doc    └──┘                                   └─────────┘
682    (return a <|> c₂) = return a :=
id      └────┘  └─┘ └┘   └────┘ 
src     └────┘   └─┘      └────┘
typ     └────┘  └─┘ └┘   └────┘ 
doc     └────┘             └────┘
683  destruct_eq_ret $ by unfold has_orelse.orelse; simp [orelse]
id   └─────────────┘                                      └────┘
src  └─────────────┘      └──────────────────────┘  └────┘└────┘└─
typ  └─────────────┘      └──────────────────────┘  └────┘└────┘└─
doc                       └──────────────────────┘  └────┘└────┘└─
txt                       └──────────────────────┘  └────┘      └─
par                       └──────────────────────┘  └────┘      └─
pid                             └────────────────┘            
st                       └────────────────────────────────────────
684  
src  
typ  
doc  
txt  
par  
pid  
st   
685  @[simp] theorem orelse_ret (c₁ : computation α) (a : α) :
id                                    └─────────┘        
src                                   └─────────┘
typ                                   └─────────┘        
doc    └──┘                           └─────────┘
686    (think c₁ <|> return a) = return a :=
id      └───┘ └┘ └─┘ └────┘    └────┘ 
src     └───┘    └─┘ └────┘     └────┘
typ     └───┘ └┘ └─┘ └────┘    └────┘ 
doc     └───┘        └────┘      └────┘
687  destruct_eq_ret $ by unfold has_orelse.orelse; simp [orelse]
id   └─────────────┘                                      └────┘
src  └─────────────┘      └──────────────────────┘  └────┘└────┘└─
typ  └─────────────┘      └──────────────────────┘  └────┘└────┘└─
doc                       └──────────────────────┘  └────┘└────┘└─
txt                       └──────────────────────┘  └────┘      └─
par                       └──────────────────────┘  └────┘      └─
pid                             └────────────────┘            
st                       └────────────────────────────────────────
688  
src  
typ  
doc  
txt  
par  
pid  
st   
689  @[simp] theorem orelse_think (c₁ c₂ : computation α) :
id                                         └─────────┘ 
src                                        └─────────┘
typ                                        └─────────┘ 
doc    └──┘                                └─────────┘
690    (think c₁ <|> think c₂) = think (c₁ <|> c₂) :=
id      └───┘ └┘ └─┘ └───┘ └┘   └───┘  └┘ └─┘ └┘
src     └───┘    └─┘ └───┘      └───┘     └─┘
typ     └───┘ └┘ └─┘ └───┘ └┘   └───┘  └┘ └─┘ └┘
doc     └───┘        └───┘       └───┘
691  destruct_eq_think $ by unfold has_orelse.orelse; simp [orelse]
id   └───────────────┘                                      └────┘
src  └───────────────┘      └──────────────────────┘  └────┘└────┘└─
typ  └───────────────┘      └──────────────────────┘  └────┘└────┘└─
doc                         └──────────────────────┘  └────┘└────┘└─
txt                         └──────────────────────┘  └────┘      └─
par                         └──────────────────────┘  └────┘      └─
pid                               └────────────────┘            
st                         └────────────────────────────────────────
692  
src  
typ  
doc  
txt  
par  
pid  
st   
693  @[simp] theorem empty_orelse (c) : (empty α <|> c) = c :=
id                                       └───┘  └─┘    
src                                      └───┘   └─┘    
typ                                      └───┘  └─┘    
doc    └──┘                              └───┘
694  begin
st   └─────
695    apply eq_of_bisim (λc₁ c₂, (empty α <|> c₂) = c₁) _ rfl,
id           └─────────┘           └───┘  └─┘            └─┘
src    └────┘└─────────┘  └─────┘ └───┘ └─┘  └┘  └──┘└─┘
typ    └────┘└─────────┘  └─────┘ └───┘└─┘  └┘  └──┘└─┘
doc    └────┘             └─────┘ └───┘      └┘   └──┘
txt    └────┘             └─────┘            └┘   └──┘
par    └────┘             └─────┘            └┘   └──┘
pid                      └─────┘            └┘   └──┘
st   ────────────────────────────────────────────────────────┘└─
696    intros s' s h, rw ←h,
id                        
src    └───────────┘  └──┘
typ    └───────────┘  └──┘
doc    └───────────┘  └──┘
txt    └───────────┘  └──┘
par    └───────────┘  └──┘
pid          └─────┘    └┘
st   ──────────────┘└─────┘└─
697    apply cases_on s; intros s; rw think_empty; simp,
id           └──────┘                └─────────┘
src    └────┘└──────┘   └──────┘  └─┘└─────────┘  └──┘
typ    └────┘└──────┘  └──────┘  └─┘└─────────┘  └──┘
doc    └────┘           └──────┘  └─┘             └──┘
txt    └────┘           └──────┘  └─┘             └──┘
par    └────┘           └──────┘  └─┘             └──┘
pid                          └┘    
st   ────────────────────────────────┘└─────────┘└────┘└─
698    rw ←think_empty,
id         └─────────┘
src    └──┘└─────────┘
typ    └──┘└─────────┘
doc    └──┘
txt    └──┘
par    └──┘
pid      └┘
st   ────────────────┘└─
699  end
st   ──┘
700  
701  @[simp] theorem orelse_empty (c : computation α) : (c <|> empty α) = c :=
id                                     └─────────┘       └─┘ └───┘    
src                                    └─────────┘         └─┘ └───┘    
typ                                    └─────────┘       └─┘ └───┘    
doc    └──┘                            └─────────┘             └───┘
702  begin
st   └─────
703    apply eq_of_bisim (λc₁ c₂, (c₂ <|> empty α) = c₁) _ rfl,
id           └─────────┘              └─┘ └───┘          └─┘
src    └────┘└─────────┘  └─────┘   └─┘└───┘ └┘  └──┘└─┘
typ    └────┘└─────────┘  └─────┘   └─┘└───┘└┘  └──┘└─┘
doc    └────┘             └─────┘      └───┘ └┘   └──┘
txt    └────┘             └─────┘            └┘   └──┘
par    └────┘             └─────┘            └┘   └──┘
pid                      └─────┘            └┘   └──┘
st   ────────────────────────────────────────────────────────┘└─
704    intros s' s h, rw ←h,
id                        
src    └───────────┘  └──┘
typ    └───────────┘  └──┘
doc    └───────────┘  └──┘
txt    └───────────┘  └──┘
par    └───────────┘  └──┘
pid          └─────┘    └┘
st   ──────────────┘└─────┘└─
705    apply cases_on s; intros s; rw think_empty; simp,
id           └──────┘                └─────────┘
src    └────┘└──────┘   └──────┘  └─┘└─────────┘  └──┘
typ    └────┘└──────┘  └──────┘  └─┘└─────────┘  └──┘
doc    └────┘           └──────┘  └─┘             └──┘
txt    └────┘           └──────┘  └─┘             └──┘
par    └────┘           └──────┘  └─┘             └──┘
pid                          └┘    
st   ────────────────────────────────┘└─────────┘└────┘└─
706    rw←think_empty,
id        └─────────┘
src    └─┘└─────────┘
typ    └─┘└─────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────┘└─
707  end
st   ──┘
708  
709  /-- `c₁ ~ c₂` asserts that `c₁` and `c₂` either both terminate with the same result,
710    or both loop forever. -/
711  def equiv (c₁ c₂ : computation α) : Prop := ∀ a, a ∈ c₁ ↔ a ∈ c₂
id                      └─────────┘                   └┘    └┘
src                     └─────────┘                            
typ                     └─────────┘                   └┘    └┘
doc                     └─────────┘
712  
713  infix ~ := equiv
id              └───┘
src             └───┘
typ             └───┘
doc             └───┘
714  
715  @[refl] theorem equiv.refl (s : computation α) : s ~ s := λ_, iff.rfl
id                                   └─────────┘              └─────┘
src    └──┘                          └─────────┘                  └─────┘
typ                                  └─────────┘              └─────┘
doc    └──┘                          └─────────┘        
716  
717  @[symm] theorem equiv.symm {s t : computation α} : s ~ t → t ~ s :=
id                                     └─────────┘            
src    └──┘                            └─────────┘               
typ                                    └─────────┘            
doc    └──┘                            └─────────┘               
718  λh a, (h a).symm
id          └──┘
src             └──┘
typ         └──┘
719  
720  @[trans] theorem equiv.trans {s t u : computation α} : s ~ t → t ~ u → s ~ u :=
id                                         └─────────┘                 
src    └───┘                               └─────────┘                      
typ                                        └─────────┘                 
doc    └───┘                               └─────────┘                      
721  λh1 h2 a, (h1 a).trans (h2 a)
id    └┘ └┘    └┘  └───┘   └┘ 
src                  └───┘
typ   └┘ └┘    └┘  └───┘   └┘ 
722  
723  theorem equiv.equivalence : equivalence (@equiv α) :=
id                               └─────────┘   └───┘ 
src                              └─────────┘   └───┘
typ                              └─────────┘   └───┘ 
doc                                            └───┘
724  ⟨@equiv.refl _, @equiv.symm _, @equiv.trans _⟩
id     └────────┘     └────────┘     └─────────┘
src    └────────┘     └────────┘     └─────────┘
typ    └────────┘     └────────┘     └─────────┘
725  
726  theorem equiv_of_mem {s t : computation α} {a} (h1 : a ∈ s) (h2 : a ∈ t) : s ~ t :=
id                               └─────────┘                               
src                              └─────────┘                                    
typ                              └─────────┘                               
doc                              └─────────┘                                      
727  λa', ⟨λma, by rw mem_unique ma h1; exact h2,
id    └┘    └┘        └────────┘ └┘ └┘        └┘
src                └─┘└────────┘      └────┘
typ   └┘    └┘     └─┘└────────┘└┘└┘  └────┘└┘
doc                └─┘                └────┘
txt                └─┘                └────┘
par                └─┘                └────┘
pid                                       
st                └────────────────────────────┘
728        λma, by rw mem_unique ma h2; exact h1⟩
id          └┘        └────────┘ └┘ └┘        └┘
src                └─┘└────────┘      └────┘
typ         └┘     └─┘└────────┘└┘└┘  └────┘└┘
doc                └─┘                └────┘
txt                └─┘                └────┘
par                └─┘                └────┘
pid                                       
st                └────────────────────────────┘
729  
730  theorem terminates_congr {c₁ c₂ : computation α}
id                                     └─────────┘ 
src                                    └─────────┘
typ                                    └─────────┘ 
doc                                    └─────────┘
731    (h : c₁ ~ c₂) : terminates c₁ ↔ terminates c₂ :=
id          └┘  └┘    └────────┘ └┘  └────────┘ └┘
src                   └────────┘     └────────┘
typ         └┘  └┘    └────────┘ └┘  └────────┘ └┘
doc                   └────────┘      └────────┘
732  exists_congr h
id   └──────────┘ 
src  └──────────┘
typ  └──────────┘ 
733  
734  theorem promises_congr {c₁ c₂ : computation α}
id                                   └─────────┘ 
src                                  └─────────┘
typ                                  └─────────┘ 
doc                                  └─────────┘
735    (h : c₁ ~ c₂) (a) : c₁ ~> a ↔ c₂ ~> a :=
id          └┘  └┘        └┘ └┘   └┘ └┘ 
src                          └┘       └┘
typ         └┘  └┘        └┘ └┘   └┘ └┘ 
doc                          └┘        └┘
736  forall_congr (λa', imp_congr (h a') iff.rfl)
id   └──────────┘   └┘  └───────┘   └┘  └─────┘
src  └──────────┘       └───────┘        └─────┘
typ  └──────────┘   └┘  └───────┘   └┘  └─────┘
737  
738  theorem get_equiv {c₁ c₂ : computation α} (h : c₁ ~ c₂)
id                              └─────────┘        └┘  └┘
src                             └─────────┘            
typ                             └─────────┘        └┘  └┘
doc                             └─────────┘            
739    [terminates c₁] [terminates c₂] : get c₁ = get c₂ :=
id      └────────┘ └┘   └────────┘ └┘    └─┘ └┘  └─┘ └┘
src     └────────┘      └────────┘       └─┘     └─┘
typ     └────────┘ └┘   └────────┘ └┘    └─┘ └┘  └─┘ └┘
doc     └────────┘      └────────┘       └─┘      └─┘
740  get_eq_of_mem _ $ (h _).2 $ get_mem _
id   └───────────┘             └─────┘
src  └───────────┘              └─────┘
typ  └───────────┘             └─────┘
741  
742  theorem think_equiv (s : computation α) : think s ~ s :=
id                            └─────────┘     └───┘   
src                           └─────────┘      └───┘   
typ                           └─────────┘     └───┘   
doc                           └─────────┘      └───┘   
743  λ a, ⟨of_think_mem, think_mem⟩
id        └──────────┘  └───────┘
src        └──────────┘  └───────┘
typ       └──────────┘  └───────┘
744  
745  theorem thinkN_equiv (s : computation α) (n) : thinkN s n ~ s :=
id                             └─────────┘         └────┘    
src                            └─────────┘          └────┘     
typ                            └─────────┘         └────┘    
doc                            └─────────┘          └────┘     
746  λ a, thinkN_mem n
id       └────────┘ 
src       └────────┘
typ      └────────┘ 
747  
748  theorem bind_congr {s1 s2 : computation α} {f1 f2 : α → computation β}
id                               └─────────┘               └─────────┘ 
src                              └─────────┘                 └─────────┘
typ                              └─────────┘               └─────────┘ 
doc                              └─────────┘                 └─────────┘
749    (h1 : s1 ~ s2) (h2 : ∀ a, f1 a ~ f2 a) : bind s1 f1 ~ bind s2 f2 :=
id           └┘  └┘            └┘   └┘     └──┘ └┘ └┘  └──┘ └┘ └┘
src                                           └──┘        └──┘
typ          └┘  └┘            └┘   └┘     └──┘ └┘ └┘  └──┘ └┘ └┘
doc                                           └──┘        └──┘
750  λ b, ⟨λh, let ⟨a, ha, hb⟩ := exists_of_mem_bind h in
id           └─┘    └┘  └┘     └────────────────┘ 
src                               └────────────────┘
typ          └─┘    └┘  └┘     └────────────────┘ 
751          mem_bind ((h1 a).1 ha) ((h2 a b).1 hb),
id           └──────┘   └┘           └┘    
src          └──────┘                       
typ          └──────┘   └┘           └┘    
752        λh, let ⟨a, ha, hb⟩ := exists_of_mem_bind h in
id            └─┘    └┘  └┘     └────────────────┘ 
src                               └────────────────┘
typ           └─┘    └┘  └┘     └────────────────┘ 
753          mem_bind ((h1 a).2 ha) ((h2 a b).2 hb)⟩
id           └──────┘   └┘           └┘    
src          └──────┘                       
typ          └──────┘   └┘           └┘    
754  
755  theorem equiv_ret_of_mem {s : computation α} {a} (h : a ∈ s) : s ~ return a :=
id                                 └─────────┘                    └────┘ 
src                                └─────────┘                        └────┘
typ                                └─────────┘                    └────┘ 
doc                                └─────────┘                         └────┘
756  equiv_of_mem h (ret_mem _)
id   └──────────┘   └─────┘
src  └──────────┘    └─────┘
typ  └──────────┘   └─────┘
757  
758  /-- `lift_rel R ca cb` is a generalization of `equiv` to relations other than
759    equality. It asserts that if `ca` terminates with `a`, then `cb` terminates with
760    some `b` such that `R a b`, and if `cb` terminates with `b` then `ca` terminates
761    with some `a` such that `R a b`. -/
762  def lift_rel (R : α → β → Prop) (ca : computation α) (cb : computation β) : Prop :=
id                                       └─────────┘         └─────────┘ 
src                                        └─────────┘          └─────────┘
typ                                      └─────────┘         └─────────┘ 
doc                                        └─────────┘          └─────────┘
763  (∀ {a}, a ∈ ca → ∃ {b}, b ∈ cb ∧ R a b) ∧
id            └┘         └┘      
src                                     
typ           └┘         └┘      
764   ∀ {b}, b ∈ cb → ∃ {a}, a ∈ ca ∧ R a b
id            └┘         └┘    
src                             
typ           └┘         └┘    
765  
766  theorem lift_rel.swap (R : α → β → Prop) (ca : computation α) (cb : computation β) :
id                                                └─────────┘         └─────────┘ 
src                                                 └─────────┘          └─────────┘
typ                                               └─────────┘         └─────────┘ 
doc                                                 └─────────┘          └─────────┘
767    lift_rel (function.swap R) cb ca ↔ lift_rel R ca cb :=
id     └──────┘  └───────────┘   └┘ └┘  └──────┘  └┘ └┘
src    └──────┘  └───────────┘           └──────┘
typ    └──────┘  └───────────┘   └┘ └┘  └──────┘  └┘ └┘
doc    └──────┘                           └──────┘
768  and_comm _ _
id   └──────┘
src  └──────┘
typ  └──────┘
769  
770  theorem lift_eq_iff_equiv (c₁ c₂ : computation α) : lift_rel (=) c₁ c₂ ↔ c₁ ~ c₂ :=
id                                      └─────────┘     └──────┘    └┘ └┘  └┘  └┘
src                                     └─────────┘      └──────┘              
typ                                     └─────────┘     └──────┘    └┘ └┘  └┘  └┘
doc                                     └─────────┘      └──────┘                
771  ⟨λ⟨h1, h2⟩ a,
id     └┘  └┘  
typ    └┘  └┘  
772    ⟨λ a1, let ⟨b, b2, ab⟩ := h1 a1 in by rwa ab,
id        └┘  └─┘                   └┘           └┘
src                                          └──┘
typ       └┘  └─┘                   └┘       └──┘└┘
doc                                          └──┘
txt                                          └──┘
par                                          └──┘
pid                                             
st                                          └─────┘
773     λ a2, let ⟨b, b1, ab⟩ := h2 a2 in by rwa ←ab⟩,
id        └┘  └─┘                   └┘            └┘
src                                          └───┘
typ       └┘  └─┘                   └┘       └───┘└┘
doc                                          └───┘
txt                                          └───┘
par                                          └───┘
pid                                             └┘
st                                          └──────┘
774  λe, ⟨λ a a1, ⟨a, (e _).1 a1, rfl⟩, λ a a2, ⟨a, (e _).2 a2, rfl⟩⟩⟩
id          └┘           └┘  └─┘      └┘           └┘  └─┘
src                              └─┘                          └─┘
typ         └┘           └┘  └─┘      └┘           └┘  └─┘
775  
776  theorem lift_rel.refl (R : α → α → Prop) (H : reflexive R) : reflexive (lift_rel R) :=
id                                               └───────┘     └───────┘  └──────┘ 
src                                                └───────┘      └───────┘  └──────┘
typ                                              └───────┘     └───────┘  └──────┘ 
doc                                                                          └──────┘
777  λ s, ⟨λ a as, ⟨a, as, H a⟩, λ b bs, ⟨b, bs, H b⟩⟩
id           └┘     └┘         └┘     └┘   
typ          └┘     └┘         └┘     └┘   
778  
779  theorem lift_rel.symm (R : α → α → Prop) (H : symmetric R) : symmetric (lift_rel R) :=
id                                               └───────┘     └───────┘  └──────┘ 
src                                                └───────┘      └───────┘  └──────┘
typ                                              └───────┘     └───────┘  └──────┘ 
doc                                                                          └──────┘
780  λ s1 s2 ⟨l, r⟩,
id     └┘ └┘   
typ    └┘ └┘   
781   ⟨λ a a2, let ⟨b, b1, ab⟩ := r a2 in ⟨b, b1, H ab⟩,
id        └┘  └─┘    └┘  └┘       └┘            
typ       └┘  └─┘    └┘  └┘       └┘            
782    λ a a1, let ⟨b, b2, ab⟩ := l a1 in ⟨b, b2, H ab⟩⟩
id        └┘  └─┘    └┘  └┘       └┘            
typ       └┘  └─┘    └┘  └┘       └┘            
783  
784  theorem lift_rel.trans (R : α → α → Prop) (H : transitive R) : transitive (lift_rel R) :=
id                                                └────────┘     └────────┘  └──────┘ 
src                                                 └────────┘      └────────┘  └──────┘
typ                                               └────────┘     └────────┘  └──────┘ 
doc                                                                             └──────┘
785  λ s1 s2 s3 ⟨l1, r1⟩ ⟨l2, r2⟩,
id     └┘ └┘ └┘ └┘  └┘  └┘  └┘
typ    └┘ └┘ └┘ └┘  └┘  └┘  └┘
786   ⟨λ a a1, let ⟨b, b2, ab⟩ := l1 a1, ⟨c, c3, bc⟩ := l2 b2 in ⟨c, c3, H ab bc⟩,
id        └┘  └─┘     └┘  └┘        └┘     └┘  └┘                      
typ       └┘  └─┘     └┘  └┘        └┘     └┘  └┘                      
787    λ c c3, let ⟨b, b2, bc⟩ := r2 c3, ⟨a, a1, ab⟩ := r1 b2 in ⟨a, a1, H ab bc⟩⟩
id        └┘  └─┘     └┘  └┘        └┘     └┘  └┘                      
typ       └┘  └─┘     └┘  └┘        └┘     └┘  └┘                      
788  
789  theorem lift_rel.equiv (R : α → α → Prop) : equivalence R → equivalence (lift_rel R)
id                                             └─────────┘   └─────────┘  └──────┘ 
src                                              └─────────┘     └─────────┘  └──────┘
typ                                            └─────────┘   └─────────┘  └──────┘ 
doc                                                                           └──────┘
790  | ⟨refl, symm, trans⟩ :=
id      └──┘  └──┘  └───┘
src     └──┘  └──┘  └───┘
typ     └──┘  └──┘  └───┘
791    ⟨lift_rel.refl R refl, lift_rel.symm R symm, lift_rel.trans R trans⟩
id      └───────────┘        └───────────┘        └────────────┘ 
src     └───────────┘         └───────────┘         └────────────┘
typ     └───────────┘        └───────────┘        └────────────┘ 
792  
793  theorem lift_rel.imp {R S : α → β → Prop} (H : ∀ {a b}, R a b → S a b) (s t) :
id                                                              
typ                                                             
794    lift_rel R s t → lift_rel S s t | ⟨l, r⟩ :=
id     └──────┘     └──────┘         
src    └──────┘         └──────┘
typ    └──────┘     └──────┘         
doc    └──────┘         └──────┘
795  ⟨λ a as, let ⟨b, bt, ab⟩ := l as in ⟨b, bt, H ab⟩,
id       └┘  └─┘    └┘  └┘       └┘            
typ      └┘  └─┘    └┘  └┘       └┘            
796   λ b bt, let ⟨a, as, ab⟩ := r bt in ⟨a, as, H ab⟩⟩
id       └┘  └─┘    └┘  └┘       └┘            
typ      └┘  └─┘    └┘  └┘       └┘            
797  
798  theorem terminates_of_lift_rel {R : α → β → Prop} {s t} :
id                                          
typ                                         
799   lift_rel R s t → (terminates s ↔ terminates t) | ⟨l, r⟩ :=
id    └──────┘      └────────┘   └────────┘        
src   └──────┘          └────────┘    └────────┘
typ   └──────┘      └────────┘   └────────┘        
doc   └──────┘          └────────┘     └────────┘
800  ⟨λ ⟨a, as⟩, let ⟨b, bt, ab⟩ := l as in ⟨b, bt⟩,
id         └┘   └─┘    └┘
typ        └┘   └─┘    └┘
801   λ ⟨b, bt⟩, let ⟨a, as, ab⟩ := r bt in ⟨a, as⟩⟩
id         └┘   └─┘    └┘
typ        └┘   └─┘    └┘
802  
803  theorem rel_of_lift_rel {R : α → β → Prop} {ca cb} :
id                                   
typ                                  
804   lift_rel R ca cb → ∀ {a b}, a ∈ ca → b ∈ cb → R a b
id    └──────┘  └┘ └┘           └┘     └┘     
src   └──────┘                              
typ   └──────┘  └┘ └┘           └┘     └┘     
doc   └──────┘
805  | ⟨l, r⟩ a b ma mb :=
id               └┘
typ              └┘
806    let ⟨b', mb', ab'⟩ := l ma in by rw mem_unique mb mb'; exact ab'
id     └─┘                                 └────────┘ └┘ └─┘        └─┘
src                                     └─┘└────────┘       └────┘   
typ    └─┘                              └─┘└────────┘└┘└─┘  └────┘└─┘
doc                                     └─┘                 └────┘   
txt                                     └─┘                 └────┘   
par                                     └─┘                 └────┘   
pid                                                                
st                                     └────────────────────────────────
807  
src  
typ  
doc  
txt  
par  
pid  
st   
808  theorem lift_rel_of_mem {R : α → β → Prop} {a b ca cb}
id                                   
typ                                  
809    (ma : a ∈ ca) (mb : b ∈ cb) (ab : R a b) : lift_rel R ca cb :=
id             └┘          └┘              └──────┘  └┘ └┘
src                                             └──────┘
typ            └┘          └┘              └──────┘  └┘ └┘
doc                                               └──────┘
810  ⟨λ a' ma', by rw mem_unique ma' ma; exact ⟨b, mb, ab⟩,
id      └┘ └─┘        └────────┘ └─┘ └┘           └┘  └┘
src                └─┘└────────┘       └────┘  └┘  └┘  
typ     └┘ └─┘     └─┘└────────┘└─┘└┘  └────┘ └┘└┘└┘└┘
doc                └─┘                 └────┘  └┘  └┘  
txt                └─┘                 └────┘  └┘  └┘  
par                └─┘                 └────┘  └┘  └┘  
pid                                          └┘  └┘  
st                └──────────────────────────────────────┘
811   λ b' mb', by rw mem_unique mb' mb; exact ⟨a, ma, ab⟩⟩
id      └┘ └─┘        └────────┘ └─┘ └┘           └┘  └┘
src                └─┘└────────┘       └────┘  └┘  └┘  
typ     └┘ └─┘     └─┘└────────┘└─┘└┘  └────┘ └┘└┘└┘└┘
doc                └─┘                 └────┘  └┘  └┘  
txt                └─┘                 └────┘  └┘  └┘  
par                └─┘                 └────┘  └┘  └┘  
pid                                          └┘  └┘  
st                └──────────────────────────────────────┘
812  
813  theorem exists_of_lift_rel_left {R : α → β → Prop} {ca cb}
id                                           
typ                                          
814    (H : lift_rel R ca cb) {a} (h : a ∈ ca) : ∃ {b}, b ∈ cb ∧ R a b :=
id          └──────┘  └┘ └┘             └┘          └┘    
src         └──────┘                                       
typ         └──────┘  └┘ └┘             └┘          └┘    
doc         └──────┘
815  H.left h
id   └───┘ 
src   └───┘
typ  └───┘ 
816  
817  theorem exists_of_lift_rel_right {R : α → β → Prop} {ca cb}
id                                            
typ                                           
818    (H : lift_rel R ca cb) {b} (h : b ∈ cb) : ∃ {a}, a ∈ ca ∧ R a b :=
id          └──────┘  └┘ └┘             └┘          └┘    
src         └──────┘                                       
typ         └──────┘  └┘ └┘             └┘          └┘    
doc         └──────┘
819  H.right h
id   └────┘ 
src   └────┘
typ  └────┘ 
820  
821  theorem lift_rel_def {R : α → β → Prop} {ca cb} : lift_rel R ca cb ↔
id                                                   └──────┘  └┘ └┘ 
src                                                    └──────┘         
typ                                                  └──────┘  └┘ └┘ 
doc                                                    └──────┘
822    (terminates ca ↔ terminates cb) ∧ ∀ {a b}, a ∈ ca → b ∈ cb → R a b :=
id      └────────┘ └┘  └────────┘ └┘            └┘     └┘     
src     └────────┘     └────────┘                         
typ     └────────┘ └┘  └────────┘ └┘            └┘     └┘     
doc     └────────┘      └────────┘
823  ⟨λh, ⟨terminates_of_lift_rel h, λ a b ma mb,
id        └────────────────────┘       └┘ └┘
src        └────────────────────┘
typ       └────────────────────┘       └┘ └┘
824    let ⟨b', mb', ab⟩ := h.left ma in by rwa mem_unique mb mb'⟩,
id     └─┘                  └───┘ └┘           └────────┘ └┘ └─┘
src                          └───┘          └──┘└────────┘  
typ    └─┘                  └───┘ └┘       └──┘└────────┘└┘└─┘
doc                                         └──┘            
txt                                         └──┘            
par                                         └──┘            
pid                                                        
st                                         └────────────────────┘
825  λ⟨l, r⟩,
id      
typ     
826   ⟨λ a ma, let ⟨b, mb⟩ := l.1 ⟨_, ma⟩ in ⟨b, mb, r ma mb⟩,
id        └┘  └─┘    └┘            └┘               └┘
src                            
typ       └┘  └─┘    └┘            └┘               └┘
827    λ b mb, let ⟨a, ma⟩ := l.2 ⟨_, mb⟩ in ⟨a, ma, r ma mb⟩⟩⟩
id        └┘  └─┘    └┘            └┘                  └┘
src                            
typ       └┘  └─┘    └┘            └┘                  └┘
828  
829  theorem lift_rel_bind {δ} (R : α → β → Prop) (S : γ → δ → Prop)
id                                                      
typ                                                     
830    {s1 : computation α} {s2 : computation β}
id           └─────────┘         └─────────┘ 
src          └─────────┘          └─────────┘
typ          └─────────┘         └─────────┘ 
doc          └─────────┘          └─────────┘
831    {f1 : α → computation γ} {f2 : β → computation δ}
id              └─────────┘            └─────────┘ 
src              └─────────┘              └─────────┘
typ             └─────────┘            └─────────┘ 
doc              └─────────┘              └─────────┘
832    (h1 : lift_rel R s1 s2) (h2 : ∀ {a b}, R a b → lift_rel S (f1 a) (f2 b))
id           └──────┘  └┘ └┘                    └──────┘   └┘    └┘ 
src          └──────┘                                 └──────┘
typ          └──────┘  └┘ └┘                    └──────┘   └┘    └┘ 
doc          └──────┘                                 └──────┘
833    : lift_rel S (bind s1 f1) (bind s2 f2) :=
id       └──────┘   └──┘ └┘ └┘   └──┘ └┘ └┘
src      └──────┘    └──┘         └──┘
typ      └──────┘   └──┘ └┘ └┘   └──┘ └┘ └┘
doc      └──────┘    └──┘         └──┘
834  let ⟨l1, r1⟩ := h1 in
id   └─┘  └┘  └┘     └┘
typ  └─┘  └┘  └┘     └┘
835  ⟨λ c cB,
id       └┘
typ      └┘
836    let ⟨a, a1, c₁⟩ := exists_of_mem_bind cB,
id     └─┘     └┘  └┘     └────────────────┘ └┘
src                       └────────────────┘
typ    └─┘     └┘  └┘     └────────────────┘ └┘
837        ⟨b, b2, ab⟩ := l1 a1,
id             └┘  └┘
typ            └┘  └┘
838        ⟨l2, r2⟩ := h2 ab,
id          └┘         └┘
typ         └┘         └┘
839        ⟨d, d2, cd⟩ := l2 c₁ in
id             └┘  └┘
typ            └┘  └┘
840    ⟨_, mem_bind b2 d2, cd⟩,
id         └──────┘
src        └──────┘
typ        └──────┘
841  λ d dB,
id      └┘
typ     └┘
842    let ⟨b, b1, d1⟩ := exists_of_mem_bind dB,
id     └─┘     └┘  └┘     └────────────────┘ └┘
src                       └────────────────┘
typ    └─┘     └┘  └┘     └────────────────┘ └┘
843        ⟨a, a2, ab⟩ := r1 b1,
id             └┘  └┘
typ            └┘  └┘
844        ⟨l2, r2⟩ := h2 ab,
id              └┘     └┘
typ             └┘     └┘
845        ⟨c, c₂, cd⟩ := r2 d1 in
id             └┘  └┘
typ            └┘  └┘
846    ⟨_, mem_bind a2 c₂, cd⟩⟩
id         └──────┘
src        └──────┘
typ        └──────┘
847  
848  @[simp] theorem lift_rel_return_left (R : α → β → Prop) (a : α) (cb : computation β) :
id                                                                      └─────────┘ 
src                                                                        └─────────┘
typ                                                                     └─────────┘ 
doc    └──┘                                                                └─────────┘
849    lift_rel R (return a) cb ↔ ∃ {b}, b ∈ cb ∧ R a b :=
id     └──────┘   └────┘   └┘        └┘    
src    └──────┘    └────┘                   
typ    └──────┘   └────┘   └┘        └┘    
doc    └──────┘    └────┘
850  ⟨λ⟨l, r⟩, l (ret_mem _),
id              └─────┘
src               └─────┘
typ             └─────┘
851   λ⟨b, mb, ab⟩,
id     
typ    
852    ⟨λ a' ma', by rw eq_of_ret_mem ma'; exact ⟨b, mb, ab⟩,
id        └┘ └─┘        └───────────┘ └─┘           └┘  └┘
src                  └─┘└───────────┘     └────┘  └┘  └┘  
typ       └┘ └─┘     └─┘└───────────┘└─┘  └────┘ └┘└┘└┘└┘
doc                  └─┘                  └────┘  └┘  └┘  
txt                  └─┘                  └────┘  └┘  └┘  
par                  └─┘                  └────┘  └┘  └┘  
pid                                             └┘  └┘  
st                  └──────────────────────────────────────┘
853     λ b' mb', ⟨_, ret_mem _, by rw mem_unique mb' mb; exact ab⟩⟩⟩
id        └┘ └─┘      └─────┘          └────────┘ └─┘ └┘        └┘
src                   └─────┘       └─┘└────────┘       └────┘
typ       └┘ └─┘      └─────┘       └─┘└────────┘└─┘└┘  └────┘└┘
doc                                 └─┘                 └────┘
txt                                 └─┘                 └────┘
par                                 └─┘                 └────┘
pid                                                         
st                                 └─────────────────────────────┘
854  
855  @[simp] theorem lift_rel_return_right (R : α → β → Prop) (ca : computation α) (b : β) :
id                                                                └─────────┘        
src                                                                 └─────────┘
typ                                                               └─────────┘        
doc    └──┘                                                         └─────────┘
856    lift_rel R ca (return b) ↔ ∃ {a}, a ∈ ca ∧ R a b :=
id     └──────┘  └┘  └────┘          └┘    
src    └──────┘       └────┘                
typ    └──────┘  └┘  └────┘          └┘    
doc    └──────┘       └────┘
857  by rw [lift_rel.swap, lift_rel_return_left]
id          └───────────┘  └──────────────────┘
src     └──┘└───────────┘└┘└──────────────────┘└─
typ     └──┘└───────────┘└┘└──────────────────┘└─
doc     └──┘             └┘                    └─
txt     └──┘             └┘                    └─
par     └──┘             └┘                    └─
pid       └┘             └┘                    
st     └────────────────┘└────────────────────┘
858  
src  
typ  
doc  
txt  
par  
pid  
st   
859  @[simp] theorem lift_rel_return (R : α → β → Prop) (a : α) (b : β) :
id                                                                
typ                                                               
doc    └──┘
860    lift_rel R (return a) (return b) ↔ R a b :=
id     └──────┘   └────┘    └────┘      
src    └──────┘    └────┘     └────┘    
typ    └──────┘   └────┘    └────┘      
doc    └──────┘    └────┘     └────┘
861  by rw [lift_rel_return_left]; exact
id          └──────────────────┘
src     └──┘└──────────────────┘  └────┘
typ     └──┘└──────────────────┘  └────┘
doc     └──┘                      └────┘
txt     └──┘                      └────┘
par     └──┘                      └────┘
pid       └┘                           
st     └───────────────────────┘└───────
862  ⟨λ⟨b', mb', ab'⟩, by rwa eq_of_ret_mem mb' at ab',
id                            └───────────┘ └─┘
src      └┘   └┘   └─┘  └──┘└───────────┘   └─────┘└─
typ      └┘   └┘   └─┘  └──┘└───────────┘└─┘└─────┘└─
doc      └┘   └┘   └─┘  └──┘                └─────┘└─
txt      └┘   └┘   └─┘  └──┘                └─────┘└─
par      └┘   └┘   └─┘  └──┘                └─────┘└─
pid      └┘   └┘   └─┘  └───┘                └────────
st   ───────────────────┘└───────────────────────────┘└─
863   λab, ⟨_, ret_mem _, ab⟩⟩
id             └─────┘
src   └──┘ └─┘└─────┘└──┘  └──
typ   └──┘ └─┘└─────┘└──┘  └──
doc   └──┘ └─┘       └──┘  └──
txt   └──┘ └─┘       └──┘  └──
par   └──┘ └─┘       └──┘  └──
pid   └──┘ └─┘       └──┘  └┘
st   ──────────────────────────
864  
src  
typ  
doc  
txt  
par  
pid  
st   
865  @[simp] theorem lift_rel_think_left (R : α → β → Prop) (ca : computation α) (cb : computation β) :
id                                                              └─────────┘         └─────────┘ 
src                                                               └─────────┘          └─────────┘
typ                                                             └─────────┘         └─────────┘ 
doc    └──┘                                                       └─────────┘          └─────────┘
866    lift_rel R (think ca) cb ↔ lift_rel R ca cb :=
id     └──────┘   └───┘ └┘  └┘  └──────┘  └┘ └┘
src    └──────┘    └───┘         └──────┘
typ    └──────┘   └───┘ └┘  └┘  └──────┘  └┘ └┘
doc    └──────┘    └───┘          └──────┘
867  and_congr (forall_congr $ λb, imp_congr ⟨of_think_mem, think_mem⟩ iff.rfl)
id   └───────┘  └──────────┘      └───────┘  └──────────┘  └───────┘  └─────┘
src  └───────┘  └──────────┘       └───────┘  └──────────┘  └───────┘  └─────┘
typ  └───────┘  └──────────┘      └───────┘  └──────────┘  └───────┘  └─────┘
868   (forall_congr $ λb, imp_congr iff.rfl $
id     └──────────┘      └───────┘ └─────┘
src    └──────────┘       └───────┘ └─────┘
typ    └──────────┘      └───────┘ └─────┘
869      exists_congr $ λ b, and_congr ⟨of_think_mem, think_mem⟩ iff.rfl)
id       └──────────┘       └───────┘  └──────────┘  └───────┘  └─────┘
src      └──────────┘        └───────┘  └──────────┘  └───────┘  └─────┘
typ      └──────────┘       └───────┘  └──────────┘  └───────┘  └─────┘
870  
871  @[simp] theorem lift_rel_think_right (R : α → β → Prop) (ca : computation α) (cb : computation β) :
id                                                               └─────────┘         └─────────┘ 
src                                                                └─────────┘          └─────────┘
typ                                                              └─────────┘         └─────────┘ 
doc    └──┘                                                        └─────────┘          └─────────┘
872    lift_rel R ca (think cb) ↔ lift_rel R ca cb :=
id     └──────┘  └┘  └───┘ └┘   └──────┘  └┘ └┘
src    └──────┘       └───┘      └──────┘
typ    └──────┘  └┘  └───┘ └┘   └──────┘  └┘ └┘
doc    └──────┘       └───┘       └──────┘
873  by rw [←lift_rel.swap R, ←lift_rel.swap R]; apply lift_rel_think_left
id           └───────────┘    └───────────┘          └─────────────────┘
src     └───┘└───────────┘ └─┘└───────────┘   └────┘└─────────────────┘
typ     └───┘└───────────┘└─┘└───────────┘  └────┘└─────────────────┘
doc     └───┘              └─┘                └────┘                   
txt     └───┘              └─┘                └────┘                   
par     └───┘              └─┘                └────┘                   
pid       └─┘              └─┘                                        
st     └───────────────────┘└────────────────┘└───────────────────────────
874  
src  
typ  
doc  
txt  
par  
pid  
st   
875  theorem lift_rel_mem_cases {R : α → β → Prop} {ca cb}
id                                      
typ                                     
876    (Ha : ∀ a ∈ ca, lift_rel R ca cb)
id                └┘  └──────┘  └┘ └┘
src                   └──────┘
typ               └┘  └──────┘  └┘ └┘
doc                    └──────┘
877    (Hb : ∀ b ∈ cb, lift_rel R ca cb) : lift_rel R ca cb :=
id                └┘  └──────┘  └┘ └┘    └──────┘  └┘ └┘
src                    └──────┘            └──────┘
typ               └┘  └──────┘  └┘ └┘    └──────┘  └┘ └┘
doc                    └──────┘            └──────┘
878  ⟨λ a ma, (Ha _ ma).left ma, λ b mb, (Hb _ mb).right mb⟩
id       └┘   └┘   └┘ └──┘  └┘     └┘   └┘   └┘ └───┘  └┘
src                    └──┘                       └───┘
typ      └┘   └┘   └┘ └──┘  └┘     └┘   └┘   └┘ └───┘  └┘
879  
880  theorem lift_rel_congr {R : α → β → Prop} {ca ca' : computation α} {cb cb' : computation β}
id                                                     └─────────┘             └─────────┘ 
src                                                      └─────────┘              └─────────┘
typ                                                    └─────────┘             └─────────┘ 
doc                                                      └─────────┘              └─────────┘
881    (ha : ca ~ ca') (hb : cb ~ cb') : lift_rel R ca cb ↔ lift_rel R ca' cb' :=
id           └┘  └─┘        └┘  └─┘    └──────┘  └┘ └┘  └──────┘  └─┘ └─┘
src                                    └──────┘          └──────┘
typ          └┘  └─┘        └┘  └─┘    └──────┘  └┘ └┘  └──────┘  └─┘ └─┘
doc                                    └──────┘           └──────┘
882  and_congr
id   └───────┘
src  └───────┘
typ  └───────┘
883    (forall_congr $ λ a, imp_congr (ha _) $ exists_congr $ λ b, and_congr (hb _) iff.rfl)
id      └──────────┘       └───────┘  └┘      └──────────┘       └───────┘  └┘    └─────┘
src     └──────────┘        └───────┘          └──────────┘        └───────┘        └─────┘
typ     └──────────┘       └───────┘  └┘      └──────────┘       └───────┘  └┘    └─────┘
884    (forall_congr $ λ b, imp_congr (hb _) $ exists_congr $ λ a, and_congr (ha _) iff.rfl)
id      └──────────┘       └───────┘  └┘      └──────────┘       └───────┘  └┘    └─────┘
src     └──────────┘        └───────┘          └──────────┘        └───────┘        └─────┘
typ     └──────────┘       └───────┘  └┘      └──────────┘       └───────┘  └┘    └─────┘
885  
886  theorem lift_rel_map {δ} (R : α → β → Prop) (S : γ → δ → Prop)
id                                                     
typ                                                    
887    {s1 : computation α} {s2 : computation β}
id           └─────────┘         └─────────┘ 
src          └─────────┘          └─────────┘
typ          └─────────┘         └─────────┘ 
doc          └─────────┘          └─────────┘
888    {f1 : α → γ} {f2 : β → δ}
id                         
typ                        
889    (h1 : lift_rel R s1 s2) (h2 : ∀ {a b}, R a b → S (f1 a) (f2 b))
id           └──────┘  └┘ └┘                      └┘    └┘ 
src          └──────┘
typ          └──────┘  └┘ └┘                      └┘    └┘ 
doc          └──────┘
890    : lift_rel S (map f1 s1) (map f2 s2) :=
id       └──────┘   └─┘ └┘ └┘   └─┘ └┘ └┘
src      └──────┘    └─┘         └─┘
typ      └──────┘   └─┘ └┘ └┘   └─┘ └┘ └┘
doc      └──────┘    └─┘         └─┘
891  by rw [←bind_ret, ←bind_ret]; apply lift_rel_bind _ _ h1; simp; exact @h2
id           └──────┘   └──────┘         └───────────┘     └┘               └┘
src     └───┘└──────┘└─┘└──────┘  └────┘└───────────┘└───┘    └──┘  └────┘   
typ     └───┘└──────┘└─┘└──────┘  └────┘└───────────┘└───┘└┘  └──┘  └────┘ └┘
doc     └───┘        └─┘          └────┘             └───┘    └──┘  └────┘   
txt     └───┘        └─┘          └────┘             └───┘    └──┘  └────┘   
par     └───┘        └─┘          └────┘             └───┘    └──┘  └────┘   
pid       └─┘        └─┘                            └───┘                  
st     └────────────┘└─────────┘└─────────────────────────────────────────────
892  
src  
typ  
doc  
txt  
par  
pid  
st   
893  theorem map_congr (R : α → α → Prop) (S : β → β → Prop)
id                                              
typ                                             
894    {s1 s2 : computation α} {f : α → β}
id              └─────────┘           
src             └─────────┘
typ             └─────────┘           
doc             └─────────┘
895    (h1 : s1 ~ s2) : map f s1 ~ map f s2 :=
id           └┘  └┘    └─┘  └┘  └─┘  └┘
src                    └─┘       └─┘
typ          └┘  └┘    └─┘  └┘  └─┘  └┘
doc                    └─┘       └─┘
896  by rw [←lift_eq_iff_equiv];
id           └───────────────┘
src     └───┘└───────────────┘
typ     └───┘└───────────────┘
doc     └───┘                 
txt     └───┘                 
par     └───┘                 
pid       └─┘                 
st     └─────────────────────┘└─
897     exact lift_rel_map eq _ ((lift_eq_iff_equiv _ _).2 h1) (λ a b, congr_arg _)
id            └──────────┘ └┘     └───────────────┘        └┘          └───────┘
src     └────┘└──────────┘└┘└─┘  └───────────────┘└──────┘  └┘  └────┘└───────┘└───
typ     └────┘└──────────┘└┘└─┘  └───────────────┘└──────┘└┘└┘  └────┘└───────┘└───
doc     └────┘              └─┘                   └──────┘  └┘  └────┘         └───
txt     └────┘              └─┘                   └──────┘  └┘  └────┘         └───
par     └────┘              └─┘                   └──────┘  └┘  └────┘         └───
pid                        └─┘                   └──────┘  └┘  └────┘         └─┘
st   ───────────────────────────────────────────────────────────────────────────────
898  
src  
typ  
doc  
txt  
par  
pid  
st   
899  def lift_rel_aux (R : α → β → Prop)
id                            
typ                           
900    (C : computation α → computation β → Prop) :
id          └─────────┘    └─────────┘ 
src         └─────────┘     └─────────┘
typ         └─────────┘    └─────────┘ 
doc         └─────────┘     └─────────┘
901    α ⊕ computation α → β ⊕ computation β → Prop
id       └─────────┘     └─────────┘ 
src       └─────────┘        └─────────┘
typ      └─────────┘     └─────────┘ 
doc        └─────────┘         └─────────┘
902  | (sum.inl a)  (sum.inl b)  := R a b
id                  └─────┘       
src                  └─────┘
typ                 └─────┘       
903  | (sum.inl a)  (sum.inr cb) := ∃ {b}, b ∈ cb ∧ R a b
id      └─────┘     └─────┘ └┘                  
src     └─────┘      └─────┘                   
typ     └─────┘     └─────┘ └┘                  
904  | (sum.inr ca) (sum.inl b)  := ∃ {a}, a ∈ ca ∧ R a b
id      └─────┘ └┘   └─────┘                  
src     └─────┘      └─────┘                   
typ     └─────┘ └┘   └─────┘                  
905  | (sum.inr ca) (sum.inr cb) := C ca cb
id              └┘   └─────┘ └┘     
src                  └─────┘
typ             └┘   └─────┘ └┘     
906  attribute [simp] lift_rel_aux
id                    └──────────┘
src                   └──────────┘
typ                   └──────────┘
doc             └──┘
907  
908  @[simp] lemma lift_rel_aux.ret_left (R : α → β → Prop)
id                                               
typ                                              
doc    └──┘
909    (C : computation α → computation β → Prop) (a cb) :
id          └─────────┘    └─────────┘ 
src         └─────────┘     └─────────┘
typ         └─────────┘    └─────────┘ 
doc         └─────────┘     └─────────┘
910    lift_rel_aux R C (sum.inl a) (destruct cb) ↔ ∃ {b}, b ∈ cb ∧ R a b :=
id     └──────────┘    └─────┘    └──────┘ └┘         └┘    
src    └──────────┘      └─────┘     └──────┘                 
typ    └──────────┘    └─────┘    └──────┘ └┘         └┘    
doc                                  └──────┘
911  begin
st   └─────
912    apply cb.cases_on (λ b, _) (λ cb, _),
id           └─────────┘
src    └────┘└─────────┘  └─────┘  └─────┘
typ    └────┘└─────────┘  └─────┘  └─────┘
doc    └────┘             └─────┘  └─────┘
txt    └────┘             └─────┘  └─────┘
par    └────┘             └─────┘  └─────┘
pid                      └─────┘  └─────┘
st   ─────────────────────────────────────┘└─
913    { exact ⟨λ h, ⟨_, ret_mem _, h⟩, λ ⟨b', mb, h⟩,
id                       └─────┘
src      └────┘  └──┘ └─┘└─────┘└──┘ └─┘ └┘  └┘  └┘ └──
typ      └────┘  └──┘ └─┘└─────┘└──┘ └─┘ └┘  └┘  └┘ └──
doc      └────┘  └──┘ └─┘       └──┘ └─┘ └┘  └┘  └┘ └──
txt      └────┘  └──┘ └─┘       └──┘ └─┘ └┘  └┘  └┘ └──
par      └────┘  └──┘ └─┘       └──┘ └─┘ └┘  └┘  └┘ └──
pid             └──┘ └─┘       └──┘ └─┘ └┘  └┘  └┘ └──
st   ───┘└─────────────────────────────────────────────
914      by rw [mem_unique (ret_mem _) mb]; exact h⟩ },
id              └────────┘  └─────┘    └┘         
src  ───┘  └──┘└────────┘ └─────┘└──┘  └──────┘ └┘
typ  ───┘  └──┘└────────┘ └─────┘└──┘└┘└──────┘└┘
doc  ───┘  └──┘                  └──┘  └──────┘ └┘
txt  ───┘  └──┘                  └──┘  └──────┘ └┘
par  ───┘  └──┘                  └──┘  └──────┘ └┘
pid  ───┘  └───┘                  └──┘  └───────┘ 
st   ─────┘└────────────────────────────┘└───────┘└┘└┘
915    { rw [destruct_think],
id           └────────────┘
src      └──┘└────────────┘
typ      └──┘└────────────┘
doc      └──┘              
txt      └──┘              
par      └──┘              
pid        └┘              
st   ─────────────────────┘└──
916      exact ⟨λ ⟨b, h, r⟩, ⟨b, think_mem h, r⟩,
id                            └───────┘
src      └────┘  └┘ └┘ └┘ └─┘  └┘└───────┘ └┘ └──
typ      └────┘  └┘└┘└┘└─┘  └┘└───────┘ └┘ └──
doc      └────┘  └┘ └┘ └┘ └─┘  └┘          └┘ └──
txt      └────┘  └┘ └┘ └┘ └─┘  └┘          └┘ └──
par      └────┘  └┘ └┘ └┘ └─┘  └┘          └┘ └──
pid             └┘ └┘ └┘ └─┘  └┘          └┘ └──
st   ─────────────────────────────────────────────
917             λ ⟨b, h, r⟩, ⟨b, of_think_mem h, r⟩⟩ }
id                            └──────────┘
src  ──────────┘ └┘ └┘ └┘ └─┘  └┘└──────────┘ └┘ └─┘
typ  ──────────┘ └┘└┘└┘└─┘  └┘└──────────┘ └┘ └─┘
doc  ──────────┘ └┘ └┘ └┘ └─┘  └┘             └┘ └─┘
txt  ──────────┘ └┘ └┘ └┘ └─┘  └┘             └┘ └─┘
par  ──────────┘ └┘ └┘ └┘ └─┘  └┘             └┘ └─┘
pid  ──────────┘ └┘ └┘ └┘ └─┘  └┘             └┘ └┘
st   ───────────────────────────────────────────────┘└─
918  end
st   ──┘
919  
920  theorem lift_rel_aux.swap (R : α → β → Prop) (C) (a b) :
id                                     
typ                                    
921    lift_rel_aux (function.swap R) (function.swap C) b a = lift_rel_aux R C a b :=
id     └──────────┘  └───────────┘    └───────────┘      └──────────┘    
src    └──────────┘  └───────────┘     └───────────┘         └──────────┘
typ    └──────────┘  └───────────┘    └───────────┘      └──────────┘    
922  by cases a with a ca; cases b with b cb; simp only [lift_rel_aux]
id                                                     └──────────┘
src     └────┘ └────────┘  └────┘ └────────┘  └─────────┘└──────────┘└─
typ     └────┘└────────┘  └────┘└────────┘  └─────────┘└──────────┘└─
doc     └────┘ └────────┘  └────┘ └────────┘  └─────────┘            └─
txt     └────┘ └────────┘  └────┘ └────────┘  └─────────┘            └─
par     └────┘ └────────┘  └────┘ └────────┘  └─────────┘            └─
pid           └────────┘        └────────┘      └──┘└┘            
st     └───────────────────────────────────────────────────────────────
923  
src  
typ  
doc  
txt  
par  
pid  
st   
924  @[simp] lemma lift_rel_aux.ret_right (R : α → β → Prop)
id                                                
typ                                               
doc    └──┘
925    (C : computation α → computation β → Prop) (b ca) :
id          └─────────┘    └─────────┘ 
src         └─────────┘     └─────────┘
typ         └─────────┘    └─────────┘ 
doc         └─────────┘     └─────────┘
926    lift_rel_aux R C (destruct ca) (sum.inl b) ↔ ∃ {a}, a ∈ ca ∧ R a b :=
id     └──────────┘    └──────┘ └┘   └─────┘          └┘    
src    └──────────┘      └──────┘      └─────┘                
typ    └──────────┘    └──────┘ └┘   └─────┘          └┘    
doc                      └──────┘
927  by rw [←lift_rel_aux.swap, lift_rel_aux.ret_left]
id           └───────────────┘  └───────────────────┘
src     └───┘└───────────────┘└┘└───────────────────┘└─
typ     └───┘└───────────────┘└┘└───────────────────┘└─
doc     └───┘                 └┘                     └─
txt     └───┘                 └┘                     └─
par     └───┘                 └┘                     └─
pid       └─┘                 └┘                     
st     └─────────────────────┘└─────────────────────┘
928  
src  
typ  
doc  
txt  
par  
pid  
st   
929  theorem lift_rel_rec.lem {R : α → β → Prop} (C : computation α → computation β → Prop)
id                                                  └─────────┘    └─────────┘ 
src                                                   └─────────┘     └─────────┘
typ                                                 └─────────┘    └─────────┘ 
doc                                                   └─────────┘     └─────────┘
930    (H : ∀ {ca cb}, C ca cb → lift_rel_aux R C (destruct ca) (destruct cb))
id             └┘ └┘    └┘ └┘   └──────────┘    └──────┘ └┘   └──────┘ └┘
src                              └──────────┘      └──────┘      └──────┘
typ            └┘ └┘    └┘ └┘   └──────────┘    └──────┘ └┘   └──────┘ └┘
doc                                                └──────┘      └──────┘
931    (ca cb) (Hc : C ca cb) (a) (ha : a ∈ ca) : lift_rel R ca cb :=
id                    └┘ └┘              └┘    └──────┘  └┘ └┘
src                                              └──────┘
typ                   └┘ └┘              └┘    └──────┘  └┘ └┘
doc                                               └──────┘
932  begin
st   └─────
933    revert cb, refine mem_rec_on ha _ (λ ca' IH, _);
id                       └────────┘ └┘
src    └───────┘  └─────┘└────────┘  └─┘  └─────────┘
typ    └───────┘  └─────┘└────────┘└┘└─┘  └─────────┘
doc    └───────┘  └─────┘            └─┘  └─────────┘
txt    └───────┘  └─────┘            └─┘  └─────────┘
par    └───────┘  └─────┘            └─┘  └─────────┘
pid          └─┘                    └─┘  └─────────┘
st   ──────────┘└───────────────────────────────────────
934    intros cb Hc; have h := H Hc,
id                              └┘
src    └──────────┘  └────────┘ 
typ    └──────────┘  └────────┘└┘
doc    └──────────┘  └────────┘ 
txt    └──────────┘  └────────┘ 
par    └──────────┘  └────────┘ 
pid          └────┘  └────┘└─┘ 
st   ─────────────────────────────┘└─
935    { simp at h, simp [h] },
id                        
src      └───────┘  └────┘ └┘
typ      └───────┘  └────┘└┘
doc      └───────┘  └────┘ └┘
txt      └───────┘  └────┘ └┘
par      └───────┘  └────┘ └┘
pid          └──┘       
st   ───┘└───────┘└─────────┘└┘
936    { have h := H Hc, simp, revert h, apply cb.cases_on (λ b, _) (λ cb', _);
id                  └┘                        └─────────┘
src      └────────┘     └──┘  └──────┘  └────┘└─────────┘  └─────┘  └──────┘
typ      └────────┘└┘  └──┘  └──────┘  └────┘└─────────┘  └─────┘  └──────┘
doc      └────────┘     └──┘  └──────┘  └────┘             └─────┘  └──────┘
txt      └────────┘     └──┘  └──────┘  └────┘             └─────┘  └──────┘
par      └────────┘     └──┘  └──────┘  └────┘             └─────┘  └──────┘
pid      └────┘└─┘                 └┘                    └─────┘  └──────┘
st   ─────────────────┘└────┘└────────┘└────────────────────────────────────────
937      intro h; simp at h; simp [h], exact IH _ h }
id                                          └┘   
src      └─────┘  └───────┘  └────┘   └────┘  └─┘ 
typ      └─────┘  └───────┘  └────┘  └────┘└┘└─┘
doc      └─────┘  └───────┘  └────┘   └────┘  └─┘ 
txt      └─────┘  └───────┘  └────┘   └────┘  └─┘ 
par      └─────┘  └───────┘  └────┘   └────┘  └─┘ 
pid           └┘      └──┘                └─┘ 
st   ───────────────────────────────┘└─────────────┘└─
938  end
st   ──┘
939  
940  theorem lift_rel_rec {R : α → β → Prop} (C : computation α → computation β → Prop)
id                                              └─────────┘    └─────────┘ 
src                                               └─────────┘     └─────────┘
typ                                             └─────────┘    └─────────┘ 
doc                                               └─────────┘     └─────────┘
941    (H : ∀ {ca cb}, C ca cb → lift_rel_aux R C (destruct ca) (destruct cb))
id             └┘ └┘    └┘ └┘   └──────────┘    └──────┘ └┘   └──────┘ └┘
src                              └──────────┘      └──────┘      └──────┘
typ            └┘ └┘    └┘ └┘   └──────────┘    └──────┘ └┘   └──────┘ └┘
doc                                                └──────┘      └──────┘
942    (ca cb) (Hc : C ca cb) : lift_rel R ca cb :=
id                    └┘ └┘    └──────┘  └┘ └┘
src                             └──────┘
typ                   └┘ └┘    └──────┘  └┘ └┘
doc                             └──────┘
943  lift_rel_mem_cases (lift_rel_rec.lem C @H ca cb Hc) (λ b hb,
id   └────────────────┘  └──────────────┘    └┘ └┘ └┘      └┘
src  └────────────────┘  └──────────────┘
typ  └────────────────┘  └──────────────┘    └┘ └┘ └┘      └┘
944   (lift_rel.swap _ _ _).2 $
id     └───────────┘       
src    └───────────┘       
typ    └───────────┘       
945   lift_rel_rec.lem (function.swap C)
id    └──────────────┘  └───────────┘ 
src   └──────────────┘  └───────────┘
typ   └──────────────┘  └───────────┘ 
946     (λ cb ca h, cast (lift_rel_aux.swap _ _ _ _).symm $ H h)
id         └┘ └┘   └──┘  └───────────────┘         └──┘     
src                 └──┘  └───────────────┘         └──┘
typ        └┘ └┘   └──┘  └───────────────┘         └──┘     
947     cb ca Hc b hb)
id      └┘ └┘ └┘  └┘
typ     └┘ └┘ └┘  └┘
948  
949  end computation